fabric.extension

Class DereferenceHelper

java.lang.Object

fabric.extension.DereferenceHelper

public class DereferenceHelper
extends java.lang.Object

A class containing code for checking access labels on dereferences.

Constructor Summary

Constructors

Constructor and Description
DereferenceHelper()

Method Summary

Modifier and Type	Method and Description
static void	checkAccess(Expr ref, FabricReferenceType targetType, LabelChecker lc, Position pos) Adds constraints to lc to reflect that ref influences a fetch of something of targetType.
static void	checkDereference(Receiver ref, LabelChecker lc, Position pos) Adds constraints to lc reflecting the fetch side effects of a dereference

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DereferenceHelper

public DereferenceHelper()

Method Detail

checkDereference

public static void checkDereference(Receiver ref,
                                    LabelChecker lc,
                                    Position pos)
                             throws SemanticException

Adds constraints to lc reflecting the fetch side effects of a dereference

Throws:

SemanticException

checkAccess

public static void checkAccess(Expr ref,
                               FabricReferenceType targetType,
                               LabelChecker lc,
                               Position pos)
                        throws SemanticException

Adds constraints to lc to reflect that ref influences a fetch of something of targetType. For example, the code

 C1 x;
 (C2) x;
 

will cause a flow from the label of x to the access label of C2; checkAccess(x, C2, ...) will add constraints reflecting that. Assumes that ref has already been label checked.

Throws:

SemanticException