|
|||||||||
PREV NEXT | FRAMES NO FRAMES |
Access
represents a Amb
of the form "P[e]"
where e must be an expression.ActsForConstraint
interface.ActsFor constraint
.Expr
s that are the arguments to
the procedure call.
Param
s, being the parameters with which
this class is instantiated.
left
to act for right
,
and add them to eqns
.
auth
left
to be less than or
equal to right
, and add them to eqns
.
AmbParam
interface.AmbPrincipalNode
interface,
representing an ambiguous conjunctive or disjunctive principal.AmbNewArray
interface.AmbParam
interface.AmbParamTypeOrAccess
interface.AmbPrincipalNode
interface.this
label node.AmbThisLabelNode
interface.AmbVarLabelNode
interface.Array
represents a Amb
of the form "P[]".Assertion
represents a condition on labels and/or principals
that is assumed to hold true.AuthConstraint
interface.AuthConstraintNode
interface.CallerConstraint
interface.baseType
updated.
CallerConstraint
interface.CallerConstraint
interface.CanonicalConstraint
.CanonicalLabelNode
interface.CanonicalPrincipal
interface.endorse
statement.CheckedEndorseStmt
interface.components
updated.
components
updated.
ConstArrayType
represents an array of base types,
whose elements cannot change after initialization.ConstArrayTypeNode
is a type node for a non-canonical
const array type.ConstArrayTypeNode
is a type node for a non-canonical
const array type.Constraint
is the superclass of label
constraints and principals constraints, which
are generated during type checking and label checking.LabelConstraintMessage
provides error messages for
label constraints.ConstraintNode
interface.CovariantLabel
interface.declassify
expression.DeclassifyExpr
interface.declassify
statement.DeclassifyStmt
interface.dims
updated.
name
.
DowngradeExpr
interface.DowngradeStmt
interface.DynamicLabel
interface.DynamicPrincipal
interface.endorse
expression.EndorseExpr
interface.endorse
statement.EndorseStmt
interface.EOF
Symbol index.
error
Symbol index.
c
.
c
.
ExceptionPath
interface.ExternalPrincipal
interface.Collection
of Equations
for this
constraint.
Collection
of Equations
for this
constraint.
Collection
of Equations
for this
constraint.
Label
associated with branching to the
location label
, with the branch kind kind
.
Label
associated with branching to the
location label
, with the branch kind kind
.
Inst
represents a Amb
of the form "P[T,U,...]".InstOrAccess
represents a Amb
of the form
"P[e]" or "P[p]".InstTypeNode
interface.Jif
interface.ArrayAccessAssign_c
represents a Java assignment expression
to an array element.ArrayAccessAssign
node.ArrayAccessAssign
node.ArrayAccess
node.ArrayAccess
node.ArrayInit
node.Assign
node.Binary
node.Block
node.Branch
node.Call
node.Call
node.JifCanonicalTypeNode
is a type node for a canonical type in Polyj.JifCanonicalTypeNode
is a type node for a canonical type in Polyj.Case
node.Cast
node.Cast
node.CheckedEndorseStmt
node.ClassBody
node.JifClassDecl
interface.JifClassDecl
node.JifClassDecl
node.Conditional
node.ConstructorCall
node.ConstructorCall
node.JifConstructor
interface.JifConstructorDecl
node.JifConstructorInstance
interface.JifContext
interface.DeclassifyExpr
node.DeclassifyStmt
node.Do
node.DowngradeExpr
node.DeclassifyStmt
node.Empty
node.EndorseExpr
node.EndorseStmt
node.Eval
node.Expr
nodes.FieldAssign
node.LocalAssign
node.FieldDecl
node.FieldDecl
node.FieldDecl
node.Field
node.Field
node.JifFieldInstance
interface.For
node.Formal
node.Formal
node.FieldAssign
node.If
node.Initializer
node.Initializer
node.Cast
node.Instanceof
node.Jif
interface.Labeled
node.Lit
or NewLabel
node.LocalAssign
node.JifMethodDecl
node.LocalDecl
node.Local
node.JifLocalInstance
interface.JifMethod
interface.JifMethodDecl
node.JifMethodDecl
node.JifMethodInstance
interface.JifParsedPolyType
interface.NewArray
node.New
node.JifNodeFactory
interface.JifParsedPolyType
interface.ProcedureDecl
node.ProcedureDecl
node.ProcedureDecl
node.Return
node.Special
node.LabelSubstitution
that performs
substitutions on Label
s and Principal
s.Switch
node.Synchronized
node.Throw
node.Throw
node.Try
node.TypeNode
node.JifTypeSystem
interface.Unary
node.Jif
interface.While
node.JoinLabel
interface.JoinLabel
interface.Label
interface.LabelChecker
class is used in the label checking of
Jif.LabelConstraint
represents a constraint on labels, which
may either be an inequality or equality constraint.LabeledType
interface.LabeledTypeNode
interface.new label
statement.NewLabel
interface.LabelNode
interface.defaultLabel
if unlabeled.
LabelSubsitution
to all labels
that occur in the AST.MeetLabel
interface.JoinLabel
interface.Name
represents a Amp
of the form "n | P.n".new label
statement.NewLabel
interface.NotTaken
is the label for paths which cannot be
taken, for example, the path that includes statements following a return statement.NotTaken
interface.ParamDecl
interface.ParamInstance
interface.ParamLabel
interface.ParamPrincipal
interface.PramaInstance
object into a label node or a
principal node.
PolicyLabel
interface.PolicyLabel
interface.JifPolyType
for the given
JifClassType jct
.
Principal
interface.PrincipalConstraint
represents a constraint on principals, which
may either be an actsfor or an equivalence constraint.new principal
expression.PrincipalInstance
represents a global principal.PrincipalInstance
interface.PrincipalNode
interface.PrincipalInstance
object into a principal node.
owner: r1,...,rn
PolicyLabel
interface.PolicyLabel
interface.reduce_goto
table.
Variables
Solver
to add constraints to.
lhs
and rhs
with the result of
lhs.subst(subst)
and rhs.subst(subst)
respectively.
lhs
and rhs
with the result of
lhs.subst(subst)
and rhs.subst(subst)
respectively.
lhs
and rhs
with the result of
lhs.subst(subst)
and rhs.subst(subst)
respectively.
SubstLabelSubst
, to be
used by substLabel(Label)
and
substPrincipal(Principal)
.
type
.
LabelSubsitution
to all labels
that occur in the AST.ReferenceType
that do not have an initializer.
UnknownLabel
interface.UnknownParam
interface.UnknownPrincipal
interface.UnwrapVisitor
rewrites the AST to remove any Wrapped
nodes resulting from the parser.List
of variable components that occur in either the
left or right hand side.
Label.variables()
.Set
of variables that occur in either the
left or right hand side.
Set
of variables that occur in either the
left or right hand side.
Set
of variables that occur in either the
left or right hand side.
VarLabel
interface.VarPrincipal
interface.JifVarInstance
object into a label node or
a principal node
Wrapper
wraps an Amb
inside an AST node so that
it can be insert in the AST.owner!: w1,...,wn
PolicyLabel
interface.PolicyLabel
interface.DynamicLabel
interface.reduce_goto
table.
|
|||||||||
PREV NEXT | FRAMES NO FRAMES |