|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.translate.GC
Field Summary | |
static VariableAccess |
allocvar
|
private static int |
assertContinueCounter
|
static Expr |
dzerolit
|
static Expr |
ec_return
|
static Expr |
ec_throw
|
static VariableAccess |
ecvar
|
static VariableAccess |
elemsvar
|
static Expr |
falselit
|
static VariableAccess |
LSvar
|
static Expr |
nulllit
|
static VariableAccess |
objectTBCvar
|
static Expr |
onelit
|
static VariableAccess |
resultvar
|
static VariableAccess |
statevar
|
static VariableAccess |
thisvar
|
static Expr |
truelit
|
static VariableAccess |
xresultvar
|
static Expr |
zerolit
|
Constructor Summary | |
GC()
|
Method Summary | |
static Expr |
and(Expr c1,
Expr c2)
|
static Expr |
and(ExprVec v)
|
static Expr |
and(int sloc,
int eloc,
Expr c1,
Expr c2)
|
static Expr |
and(int sloc,
int eloc,
ExprVec v)
|
static Expr |
andx(Expr c1,
Expr c2)
|
private static GuardedCmd |
assertPredicate(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
int auxLoc,
java.lang.Object aux)
|
static GuardedCmd |
assume(Expr p)
|
static GuardedCmd |
assumeAnnotation(int locPragmaDecl,
Expr p)
|
static Condition |
assumeCondition(Expr pred,
int locPragmaDecl)
|
static GuardedCmd |
assumeNegation(Expr p)
|
static GuardedCmd |
block(GenericVarDeclVec v,
GuardedCmd g)
|
static GuardedCmd |
blockL(Stmt label,
GuardedCmd g)
|
static GuardedCmd |
boxPopFromStackVector(StackVector s)
Pops two command sequences off s , call them a
and b . |
static Expr |
cast(Expr e,
Type t)
|
static GuardedCmd |
check(int locUse,
Condition cond)
See description of check above. |
static GuardedCmd |
check(int locUse,
Condition cond,
java.lang.Object aux)
See description of check above. |
static GuardedCmd |
check(int locUse,
int errorName,
Expr pred,
int locPragmaDecl)
Creates an assert, assume, or skip command, depending on the kind of given error name and locations, and depending on what checks are enabled where. |
static GuardedCmd |
check(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
int auxLoc,
java.lang.Object aux)
|
static GuardedCmd |
check(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
java.lang.Object aux)
|
static GuardedCmd |
choosecmd(GuardedCmd a,
GuardedCmd b)
|
static Condition |
condition(int label,
Expr pred,
int locPragmaDecl)
|
static GuardedCmd |
fail()
|
static Expr |
forall(GenericVarDecl v,
Expr e)
|
static Expr |
forall(GenericVarDecl v,
Expr range,
Expr e)
|
static Expr |
forall(GenericVarDecl v,
Expr e,
ExprVec nopats)
|
static Expr |
forall(GenericVarDeclVec v,
Expr range,
Expr e)
|
static Expr |
forall(int sloc,
int eloc,
GenericVarDecl v,
Expr range,
Expr e)
|
static Expr |
forall(int sloc,
int eloc,
GenericVarDecl v,
Expr range,
Expr e,
ExprVec nopats)
|
static Expr |
forallwithpats(GenericVarDecl v,
Expr e,
ExprVec pats)
|
static Condition |
freeCondition(Expr pred,
int locPragmaDecl)
|
static GuardedCmd |
gets(VariableAccess lhs,
Expr rhs)
|
static GuardedCmd |
ifcmd(Expr t,
GuardedCmd c,
GuardedCmd a)
|
static Expr |
implies(Expr c0,
Expr c1)
|
static Expr |
implies(int sloc,
int eloc,
Expr c0,
Expr c1)
|
static boolean |
isBooleanLiteral(Expr e,
boolean b)
Returns true when e is a boolean
literal expression whose value is b . |
static boolean |
isFalse(Expr e)
Returns true only if e represents an
expression equivalent to false . |
static boolean |
isSimple(Expr e)
|
static LoopCmd |
loop(int sLoop,
int eLoop,
int locHotspot,
java.util.Hashtable oldmap,
ConditionVec J,
DecreasesInfoVec decs,
LocalVarDeclVec skolemConsts,
ExprVec P,
GenericVarDeclVec tempVars,
GuardedCmd B,
GuardedCmd S)
|
static VariableAccess |
makeFormalPara(java.lang.String name)
|
static VariableAccess |
makeFormalPara(java.lang.String name,
Type type)
|
static VariableAccess |
makeFormalPara(java.lang.String name,
Type type,
int locId)
|
static Identifier |
makeFullLabel(java.lang.String name,
int locPragmaDecl,
int locUse)
|
static Identifier |
makeLabel(java.lang.String name,
int locPragmaDecl,
int locUse)
|
static Identifier |
makeLabel(java.lang.String name,
int locPragmaDecl,
int auxLoc,
int locUse)
|
static VariableAccess |
makeVar(Identifier name)
|
static VariableAccess |
makeVar(Identifier name,
int locId)
|
static VariableAccess |
makeVar(java.lang.String name)
|
static VariableAccess |
makeVar(java.lang.String name,
int locId)
|
static Expr |
nary(Identifier id,
Expr e)
|
static Expr |
nary(Identifier id,
Expr e1,
Expr e2)
|
static Expr |
nary(Identifier id,
ExprVec ev)
|
static Expr |
nary(int tag,
Expr e)
|
static Expr |
nary(int tag,
Expr e1,
Expr e2)
|
static Expr |
nary(int tag,
Expr e1,
Expr e2,
Expr e3)
|
static Expr |
nary(int tag,
ExprVec ev)
|
static Expr |
nary(int sloc,
int eloc,
Identifier id,
ExprVec ev)
|
static Expr |
nary(int sloc,
int eloc,
int tag,
Expr e)
|
static Expr |
nary(int sloc,
int eloc,
int tag,
Expr e1,
Expr e2)
|
static Expr |
nary(int sloc,
int eloc,
int tag,
Expr e1,
Expr e2,
Expr e3)
|
static Expr |
nary(int sloc,
int eloc,
int tag,
ExprVec ev)
|
static Expr |
not(Expr c)
|
static Expr |
not(int sloc,
int eloc,
Expr c)
|
static Expr |
or(Expr c1,
Expr c2)
|
static Expr |
or(ExprVec v)
|
static Expr |
or(int sloc,
int eloc,
Expr c1,
Expr c2)
|
static Expr |
or(int sloc,
int eloc,
ExprVec v)
|
static Expr |
quantifiedExpr(int sloc,
int eloc,
int tag,
GenericVarDecl v,
Expr range,
Expr e,
ExprVec nopats,
ExprVec pats)
|
static Expr |
quantifiedExpr(int sloc,
int eloc,
int tag,
GenericVarDeclVec vs,
Expr range,
Expr e,
ExprVec nopats,
ExprVec pats)
|
static GuardedCmd |
raise()
|
static GuardedCmd |
restoreFrom(VariableAccess lhs,
Expr rhs)
|
static Expr |
select(Expr c0,
Expr c1)
|
private static boolean |
selectiveAdd(ExprVec to,
ExprVec from,
Expr bot,
Expr top,
int naryTagMerge)
Adds elements to to from from .
|
static GuardedCmd |
seq(GuardedCmd g1,
GuardedCmd g2)
Requires 0 < cmds.size() . |
static GuardedCmd |
seq(GuardedCmd g1,
GuardedCmd g2,
GuardedCmd g3)
|
static GuardedCmd |
seq(GuardedCmd g1,
GuardedCmd g2,
GuardedCmd g3,
GuardedCmd g4)
|
static GuardedCmd |
seq(GuardedCmdVec cmds)
May mutilate contents of cmds . |
static GuardedCmd |
skip()
|
static GuardedCmd |
subgets(VariableAccess lhs,
Expr index,
Expr rhs)
|
static Expr |
subst(GenericVarDecl var,
Expr val,
Expr target)
|
static Expr |
subst(int sloc,
int eloc,
GenericVarDecl var,
Expr val,
Expr target)
|
static Expr |
subst(int sloc,
int eloc,
java.util.Hashtable subst,
Expr target)
|
static GuardedCmd |
subsubgets(VariableAccess lhs,
Expr array,
Expr index,
Expr rhs)
|
static Expr |
symlit(Stmt s,
java.lang.String prefix)
|
static Expr |
symlit(java.lang.String s)
|
static GuardedCmd |
trycmd(GuardedCmd c,
GuardedCmd a)
|
static Expr |
typeExpr(Type t)
|
static Expr |
zeroequiv(Type t)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
private static int assertContinueCounter
public static final Expr nulllit
public static final Expr zerolit
public static final Expr onelit
public static final Expr truelit
public static final Expr falselit
public static final Expr dzerolit
public static final VariableAccess allocvar
public static final VariableAccess ecvar
public static final VariableAccess elemsvar
public static final VariableAccess resultvar
public static final VariableAccess xresultvar
public static final VariableAccess objectTBCvar
public static final VariableAccess statevar
public static VariableAccess LSvar
public static final VariableAccess thisvar
public static final Expr ec_throw
public static final Expr ec_return
Constructor Detail |
public GC()
Method Detail |
public static GuardedCmd block(GenericVarDeclVec v, GuardedCmd g)
public static GuardedCmd blockL(Stmt label, GuardedCmd g)
public static GuardedCmd seq(GuardedCmd g1, GuardedCmd g2)
0 < cmds.size()
.
public static GuardedCmd seq(GuardedCmd g1, GuardedCmd g2, GuardedCmd g3)
public static GuardedCmd seq(GuardedCmd g1, GuardedCmd g2, GuardedCmd g3, GuardedCmd g4)
public static GuardedCmd seq(GuardedCmdVec cmds)
cmds
. The caller is expected
not to use cmds
after this call.
public static GuardedCmd gets(VariableAccess lhs, Expr rhs)
public static GuardedCmd subgets(VariableAccess lhs, Expr index, Expr rhs)
public static GuardedCmd subsubgets(VariableAccess lhs, Expr array, Expr index, Expr rhs)
public static GuardedCmd restoreFrom(VariableAccess lhs, Expr rhs)
public static GuardedCmd raise()
public static GuardedCmd skip()
public static LoopCmd loop(int sLoop, int eLoop, int locHotspot, java.util.Hashtable oldmap, ConditionVec J, DecreasesInfoVec decs, LocalVarDeclVec skolemConsts, ExprVec P, GenericVarDeclVec tempVars, GuardedCmd B, GuardedCmd S)
public static GuardedCmd ifcmd(Expr t, GuardedCmd c, GuardedCmd a)
public static GuardedCmd boxPopFromStackVector(StackVector s)
s
, call them a
and b
. Then returns the box composition of these
commands, that is, a [] b
.
public static GuardedCmd choosecmd(GuardedCmd a, GuardedCmd b)
public static GuardedCmd trycmd(GuardedCmd c, GuardedCmd a)
public static boolean isBooleanLiteral(Expr e, boolean b)
true
when e
is a boolean
literal expression whose value is b
.
public static boolean isFalse(Expr e)
true
only if e
represents an
expression equivalent to false
. This method may
return false
under any circumstance, but tries to
use cheap methods to figure out whether e
is equivalent
to false
, in which case true
is returned.
public static GuardedCmd check(int locUse, int errorName, Expr pred, int locPragmaDecl)
check
method.
In the first version, errorName
is the error name
(that is, the tag constant of the type of check), pred
evaluates to false
if the check goes wrong,
locUse
is the source location of the command or
expression that can go wrong, and locPragmaDecl
is
the location of the associated pragma, if any (or Location.NULL
if not applicable).
In the second version, errorName
, pred
,
and locPragmaDecl
are taken from the components of the
given condition cond
.
public static GuardedCmd check(int locUse, int errorName, Expr pred, int locPragmaDecl, java.lang.Object aux)
public static GuardedCmd check(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc, java.lang.Object aux)
public static GuardedCmd check(int locUse, Condition cond)
check
above.
public static GuardedCmd check(int locUse, Condition cond, java.lang.Object aux)
check
above.
public static Condition condition(int label, Expr pred, int locPragmaDecl)
public static Condition freeCondition(Expr pred, int locPragmaDecl)
public static Condition assumeCondition(Expr pred, int locPragmaDecl)
public static GuardedCmd assumeAnnotation(int locPragmaDecl, Expr p)
public static GuardedCmd assume(Expr p)
public static GuardedCmd assumeNegation(Expr p)
public static GuardedCmd fail()
private static GuardedCmd assertPredicate(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc, java.lang.Object aux)
public static Identifier makeLabel(java.lang.String name, int locPragmaDecl, int auxLoc, int locUse)
public static Identifier makeLabel(java.lang.String name, int locPragmaDecl, int locUse)
public static Identifier makeFullLabel(java.lang.String name, int locPragmaDecl, int locUse)
public static Expr subst(int sloc, int eloc, java.util.Hashtable subst, Expr target)
public static Expr subst(int sloc, int eloc, GenericVarDecl var, Expr val, Expr target)
public static Expr subst(GenericVarDecl var, Expr val, Expr target)
public static Expr symlit(java.lang.String s)
public static Expr symlit(Stmt s, java.lang.String prefix)
public static Expr zeroequiv(Type t)
public static VariableAccess makeVar(Identifier name, int locId)
public static VariableAccess makeVar(java.lang.String name, int locId)
public static VariableAccess makeFormalPara(java.lang.String name, Type type, int locId)
public static VariableAccess makeVar(java.lang.String name)
public static VariableAccess makeVar(Identifier name)
public static VariableAccess makeFormalPara(java.lang.String name, Type type)
public static VariableAccess makeFormalPara(java.lang.String name)
public static Expr typeExpr(Type t)
public static Expr cast(Expr e, Type t)
public static Expr nary(int tag, Expr e)
public static Expr nary(int sloc, int eloc, int tag, Expr e)
public static Expr nary(int tag, Expr e1, Expr e2)
public static Expr nary(int sloc, int eloc, int tag, Expr e1, Expr e2)
public static Expr nary(int tag, Expr e1, Expr e2, Expr e3)
public static Expr nary(int sloc, int eloc, int tag, Expr e1, Expr e2, Expr e3)
public static Expr nary(int tag, ExprVec ev)
public static Expr nary(Identifier id, ExprVec ev)
public static Expr nary(Identifier id, Expr e)
public static Expr nary(Identifier id, Expr e1, Expr e2)
public static Expr nary(int sloc, int eloc, Identifier id, ExprVec ev)
public static Expr nary(int sloc, int eloc, int tag, ExprVec ev)
public static Expr select(Expr c0, Expr c1)
public static Expr not(Expr c)
public static Expr not(int sloc, int eloc, Expr c)
public static Expr and(Expr c1, Expr c2)
public static Expr andx(Expr c1, Expr c2)
public static Expr and(int sloc, int eloc, Expr c1, Expr c2)
public static Expr and(ExprVec v)
public static Expr and(int sloc, int eloc, ExprVec v)
public static Expr or(Expr c1, Expr c2)
public static Expr or(int sloc, int eloc, Expr c1, Expr c2)
public static Expr or(ExprVec v)
public static Expr or(int sloc, int eloc, ExprVec v)
public static Expr implies(Expr c0, Expr c1)
public static Expr implies(int sloc, int eloc, Expr c0, Expr c1)
public static Expr forall(GenericVarDecl v, Expr e)
public static Expr forall(GenericVarDecl v, Expr range, Expr e)
public static Expr forall(GenericVarDeclVec v, Expr range, Expr e)
public static Expr forall(GenericVarDecl v, Expr e, ExprVec nopats)
public static Expr forallwithpats(GenericVarDecl v, Expr e, ExprVec pats)
public static Expr forall(int sloc, int eloc, GenericVarDecl v, Expr range, Expr e)
public static Expr forall(int sloc, int eloc, GenericVarDecl v, Expr range, Expr e, ExprVec nopats)
public static Expr quantifiedExpr(int sloc, int eloc, int tag, GenericVarDecl v, Expr range, Expr e, ExprVec nopats, ExprVec pats)
public static Expr quantifiedExpr(int sloc, int eloc, int tag, GenericVarDeclVec vs, Expr range, Expr e, ExprVec nopats, ExprVec pats)
public static boolean isSimple(Expr e)
private static boolean selectiveAdd(ExprVec to, ExprVec from, Expr bot, Expr top, int naryTagMerge)
to
from from
.
Elements equal to bot are dropped. If an element equal to top is
encountered, true is returned and to is undefined. If top is
never encountered, false is returned. If from contains an
NaryExpr with tag naryTagMerge, the components of that NaryExpr
are treated in a similar manner.
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |