|
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 NEXT | FRAMES NO FRAMES |
Packages that use GuardedCmd | |
escjava | |
escjava.ast | |
escjava.pa | |
escjava.sp | |
escjava.translate |
Uses of GuardedCmd in escjava |
Methods in escjava that return GuardedCmd | |
protected GuardedCmd |
Main.computeBody(RoutineDecl r,
InitialState initState)
This method computes the guarded command (including assuming the precondition, the translated body, the checked postcondition, and the modifies constraints) for the method or constructor r in scope scope . |
Uses of GuardedCmd in escjava.ast |
Subclasses of GuardedCmd in escjava.ast | |
class |
AssignCmd
|
class |
Call
|
class |
CmdCmdCmd
|
class |
DynInstCmd
|
class |
ExprCmd
|
class |
GetsCmd
|
class |
LoopCmd
|
class |
RestoreFromCmd
|
class |
SeqCmd
|
class |
SimpleCmd
|
class |
SubGetsCmd
|
class |
SubSubGetsCmd
|
class |
VarInCmd
|
Fields in escjava.ast declared as GuardedCmd | |
GuardedCmd |
VarInCmd.g
|
GuardedCmd |
LoopCmd.guard
|
GuardedCmd |
LoopCmd.body
|
GuardedCmd |
LoopCmd.desugared
|
private GuardedCmd[] |
GuardedCmdVec.elements
* Instance fields: * * |
GuardedCmd |
DynInstCmd.g
|
GuardedCmd |
CmdCmdCmd.g1
|
GuardedCmd |
CmdCmdCmd.g2
|
GuardedCmd |
Call.desugared
|
Methods in escjava.ast that return GuardedCmd | |
GuardedCmd |
GuardedCmdVec.elementAt(int index)
* Other methods: * * |
GuardedCmd[] |
GuardedCmdVec.toArray()
|
GuardedCmd |
GuardedCmdVec.pop()
|
Methods in escjava.ast with parameters of type GuardedCmd | |
abstract java.lang.Object |
VisitorArgResult.visitGuardedCmd(GuardedCmd x,
java.lang.Object o)
|
abstract void |
Visitor.visitGuardedCmd(GuardedCmd x)
|
static VarInCmd |
VarInCmd.make(GenericVarDeclVec v,
GuardedCmd g)
|
static LoopCmd |
LoopCmd.make(int locStart,
int locEnd,
int locHotspot,
java.util.Hashtable oldmap,
ConditionVec invariants,
DecreasesInfoVec decreases,
LocalVarDeclVec skolemConstants,
ExprVec predicates,
GenericVarDeclVec tempVars,
GuardedCmd guard,
GuardedCmd body)
|
static GuardedCmdVec |
GuardedCmdVec.make(GuardedCmd[] els)
|
void |
GuardedCmdVec.setElementAt(GuardedCmd x,
int index)
|
boolean |
GuardedCmdVec.contains(GuardedCmd x)
|
void |
GuardedCmdVec.addElement(GuardedCmd x)
|
boolean |
GuardedCmdVec.removeElement(GuardedCmd x)
|
void |
GuardedCmdVec.insertElementAt(GuardedCmd obj,
int index)
|
static void |
EscPrettyPrint.print(GuardedCmd g)
|
void |
EscPrettyPrint.print(java.io.OutputStream o,
int ind,
GuardedCmd g)
Print a guarded command. |
static DynInstCmd |
DynInstCmd.make(java.lang.String s,
GuardedCmd g)
|
static CmdCmdCmd |
CmdCmdCmd.make(int cmd,
GuardedCmd g1,
GuardedCmd g2)
|
Constructors in escjava.ast with parameters of type GuardedCmd | |
GuardedCmdVec(GuardedCmd[] els)
* Private constructors: * * |
Uses of GuardedCmd in escjava.pa |
Fields in escjava.pa declared as GuardedCmd | |
private GuardedCmd |
PredicateAbstraction.body
|
private GuardedCmd |
PredicateAbstraction.bodyDesugared
|
private GuardedCmd |
PredicateAbstraction.havoc
|
Methods in escjava.pa that return GuardedCmd | |
(package private) static GuardedCmd |
Traverse.computeHelper(GuardedCmd g,
GuardedCmd context,
Set env)
|
(package private) static GuardedCmd |
PredicateAbstraction.abstractLoop(LoopCmd g,
GuardedCmd context,
Set env)
|
private GuardedCmd |
PredicateAbstraction.abstractLoopHelper(GuardedCmd context,
Set env)
|
Methods in escjava.pa with parameters of type GuardedCmd | |
static void |
Traverse.compute(GuardedCmd g,
InitialState initState,
Translate tr)
|
private static void |
Traverse.desugarLoops(GuardedCmd g,
Translate tr)
|
(package private) static GuardedCmd |
Traverse.computeHelper(GuardedCmd g,
GuardedCmd context,
Set env)
|
(package private) static GuardedCmd |
PredicateAbstraction.abstractLoop(LoopCmd g,
GuardedCmd context,
Set env)
|
private GuardedCmd |
PredicateAbstraction.abstractLoopHelper(GuardedCmd context,
Set env)
|
Constructors in escjava.pa with parameters of type GuardedCmd | |
GCProver(mocha.wrappers.jbdd.jbddManager bddManager,
ExprVec loopPredicates,
GuardedCmd g,
GCProver oldProver)
|
Uses of GuardedCmd in escjava.sp |
Methods in escjava.sp that return GuardedCmd | |
static GuardedCmd |
DSA.dsa(GuardedCmd g)
|
static GuardedCmd |
DSA.dsa(GuardedCmd g,
VarMapPair out)
|
private static GuardedCmd |
DSA.dsa(GuardedCmd g,
VarMap map,
VarMapPair out,
java.lang.String dynInstPrefix,
RefInt preOrderCount,
java.util.Hashtable lastVarUse)
Parameters preOrderCount and lastVarUse
are used to perform a dead-variable analysis on variables, so that
merges of variables can be smaller. |
Methods in escjava.sp with parameters of type GuardedCmd | |
static Expr |
SPVC.compute(GuardedCmd g)
|
private Expr |
SPVC.computeNotWrong(GuardedCmd root)
|
static Expr |
SPVC.computeN(GuardedCmd g)
|
private NXW |
SPVC.calcNxw(GuardedCmd g)
|
static GuardedCmd |
DSA.dsa(GuardedCmd g)
|
static GuardedCmd |
DSA.dsa(GuardedCmd g,
VarMapPair out)
|
private static GuardedCmd |
DSA.dsa(GuardedCmd g,
VarMap map,
VarMapPair out,
java.lang.String dynInstPrefix,
RefInt preOrderCount,
java.util.Hashtable lastVarUse)
Parameters preOrderCount and lastVarUse
are used to perform a dead-variable analysis on variables, so that
merges of variables can be smaller. |
private static void |
DSA.computeLastVarUses(GuardedCmd g,
RefInt preOrderCount,
java.util.Hashtable lastVarUse)
|
private static void |
DSA.doPreOrderCount(GuardedCmd g,
RefInt preOrderCount)
|
Uses of GuardedCmd in escjava.translate |
Methods in escjava.translate that return GuardedCmd | |
GuardedCmd |
Translate.trBody(RoutineDecl rd,
FindContributors scope,
java.util.Hashtable premap,
Set predictedSynTargs,
Translate inlineParent,
boolean issueCautions)
Translates the body of a method or constructor, as described in ESCJ 16, section 8. |
private GuardedCmd |
Translate.spill()
Pops temporaries and code, and makes these into a VARINCMD command that is returned. |
private GuardedCmd |
Translate.opBlockCmd(Expr label)
Reduces number of stack marks by 1. |
private GuardedCmd |
Translate.wrapUpUnrolledIteration(java.lang.String locString,
int iteration,
GenericVarDeclVec tempVars)
|
GuardedCmd |
Translate.modifyATargets(Set aTargets,
int loc)
targets is set of GenericVarDecls. aTargets is set of ATargets. |
GuardedCmd |
Translate.modify(Set simpleTargets,
int loc)
|
private GuardedCmd |
Translate.traceInfoLabelCmd(ASTNode ast,
java.lang.String traceInfoTag)
|
private GuardedCmd |
Translate.traceInfoLabelCmd(ASTNode ast,
java.lang.String traceInfoTag,
int loc)
|
private GuardedCmd |
Translate.traceInfoLabelCmd(int sloc,
int eloc,
java.lang.String traceInfoTag,
int loc)
|
private GuardedCmd |
Translate.traceInfoLabelCmd(int sloc,
int eloc,
java.lang.String traceInfoTag,
java.lang.String sortSeq)
|
private GuardedCmd |
Translate.cloneGuardedCommand(GuardedCmd gc)
This method returns a guarded command G that is like
gc except that where gc contains a mutable command,
G contains a fresh copy of that command. |
private GuardedCmd |
Translate.popDeclBlock()
Pops the code and declared local variables, makes these into a command (usually a VAR .. |
private GuardedCmd |
Translate.modify(VariableAccess va,
int loc)
Modifies a GC designator. |
private GuardedCmd |
Translate.modify(Expr e,
java.util.Hashtable pt,
int loc)
|
private static GuardedCmd |
Translate.substituteGC(java.util.Hashtable pt,
GuardedCmd gc)
When a call is inlined, we need to substitute the new names given to its formal parameters for its original names in the inlined body. |
static GuardedCmd |
GetSpec.surroundBodyBySpec(GuardedCmd body,
Spec spec,
FindContributors scope,
Set syntargets,
java.util.Hashtable premap,
int locEndCurlyBrace)
Returns a command that first does an assume for each
precondition in spec , then does body , then
checks the postconditions of spec , and finally checks the
modifies constraints implied by spec . |
static GuardedCmd |
GC.block(GenericVarDeclVec v,
GuardedCmd g)
|
static GuardedCmd |
GC.blockL(Stmt label,
GuardedCmd g)
|
static GuardedCmd |
GC.seq(GuardedCmd g1,
GuardedCmd g2)
Requires 0 < cmds.size() . |
static GuardedCmd |
GC.seq(GuardedCmd g1,
GuardedCmd g2,
GuardedCmd g3)
|
static GuardedCmd |
GC.seq(GuardedCmd g1,
GuardedCmd g2,
GuardedCmd g3,
GuardedCmd g4)
|
static GuardedCmd |
GC.seq(GuardedCmdVec cmds)
May mutilate contents of cmds . |
static GuardedCmd |
GC.gets(VariableAccess lhs,
Expr rhs)
|
static GuardedCmd |
GC.subgets(VariableAccess lhs,
Expr index,
Expr rhs)
|
static GuardedCmd |
GC.subsubgets(VariableAccess lhs,
Expr array,
Expr index,
Expr rhs)
|
static GuardedCmd |
GC.restoreFrom(VariableAccess lhs,
Expr rhs)
|
static GuardedCmd |
GC.raise()
|
static GuardedCmd |
GC.skip()
|
static GuardedCmd |
GC.ifcmd(Expr t,
GuardedCmd c,
GuardedCmd a)
|
static GuardedCmd |
GC.boxPopFromStackVector(StackVector s)
Pops two command sequences off s , call them a
and b . |
static GuardedCmd |
GC.choosecmd(GuardedCmd a,
GuardedCmd b)
|
static GuardedCmd |
GC.trycmd(GuardedCmd c,
GuardedCmd a)
|
static GuardedCmd |
GC.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 |
GC.check(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
java.lang.Object aux)
|
static GuardedCmd |
GC.check(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
int auxLoc,
java.lang.Object aux)
|
static GuardedCmd |
GC.check(int locUse,
Condition cond)
See description of check above. |
static GuardedCmd |
GC.check(int locUse,
Condition cond,
java.lang.Object aux)
See description of check above. |
static GuardedCmd |
GC.assumeAnnotation(int locPragmaDecl,
Expr p)
|
static GuardedCmd |
GC.assume(Expr p)
|
static GuardedCmd |
GC.assumeNegation(Expr p)
|
static GuardedCmd |
GC.fail()
|
private static GuardedCmd |
GC.assertPredicate(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
int auxLoc,
java.lang.Object aux)
|
Methods in escjava.translate with parameters of type GuardedCmd | |
private void |
Translate.makeLoop(int sLoop,
int eLoop,
int locHotspot,
GenericVarDeclVec tempVars,
GuardedCmd guard,
GuardedCmd body,
ExprStmtPragmaVec J,
ExprStmtPragmaVec decreases,
LocalVarDeclVec skolemConsts,
ExprStmtPragmaVec P,
Expr label)
Appends to code commands that make up a loop with nominal body
guard;body , where label is raised within
body to terminate the loop. |
private GuardedCmd |
Translate.cloneGuardedCommand(GuardedCmd gc)
This method returns a guarded command G that is like
gc except that where gc contains a mutable command,
G contains a fresh copy of that command. |
private static GuardedCmd |
Translate.substituteGC(java.util.Hashtable pt,
GuardedCmd gc)
When a call is inlined, we need to substitute the new names given to its formal parameters for its original names in the inlined body. |
static void |
Translate.addTraceLabelSequenceNumbers(GuardedCmd gc)
Destructively change the trace labels in gc to insert sequence
numbers that are used by the ErrorMsg class in printing trace labels in the
correct execution order. |
private static int |
Translate.orderTraceLabels(GuardedCmd gc,
int count)
Walk through the guarded command translation of a method, adding unique number to its location sequence, in order to sort trace labels in order of execution. |
static Set |
Targets.normal(GuardedCmd gc)
Returns the set of normal targets of gc .
|
static Set |
Targets.direct(GuardedCmd gc)
Returns the set of variables that are direct normal targets in gc , that is, that are modified in some assignment
statement, not call statement, in gc . |
private static void |
Targets.simpleTargets(GuardedCmd gc,
Set set,
boolean includeCallTargets)
Adds SimpleTargets[[ gc ]] (as defined in ESCJ 16)
to set . |
static GuardedCmd |
GetSpec.surroundBodyBySpec(GuardedCmd body,
Spec spec,
FindContributors scope,
Set syntargets,
java.util.Hashtable premap,
int locEndCurlyBrace)
Returns a command that first does an assume for each
precondition in spec , then does body , then
checks the postconditions of spec , and finally checks the
modifies constraints implied by spec . |
static void |
GCSanity.check(GuardedCmd g)
|
private static void |
GCSanity.checkDeclsAndUses(GuardedCmd g,
Set edci,
Set cdni,
Set euei,
Set uuei,
java.lang.String inflection,
Set sp)
Checks that there are no duplicate definitions of local variables, including implicit outermost declarations and considering dynamic inflections. |
static GuardedCmd |
GC.block(GenericVarDeclVec v,
GuardedCmd g)
|
static GuardedCmd |
GC.blockL(Stmt label,
GuardedCmd g)
|
static GuardedCmd |
GC.seq(GuardedCmd g1,
GuardedCmd g2)
Requires 0 < cmds.size() . |
static GuardedCmd |
GC.seq(GuardedCmd g1,
GuardedCmd g2,
GuardedCmd g3)
|
static GuardedCmd |
GC.seq(GuardedCmd g1,
GuardedCmd g2,
GuardedCmd g3,
GuardedCmd g4)
|
static LoopCmd |
GC.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 GuardedCmd |
GC.ifcmd(Expr t,
GuardedCmd c,
GuardedCmd a)
|
static GuardedCmd |
GC.choosecmd(GuardedCmd a,
GuardedCmd b)
|
static GuardedCmd |
GC.trycmd(GuardedCmd c,
GuardedCmd a)
|
static Expr |
Ejp.compute(GuardedCmd g,
Expr normal,
Expr exceptional)
|
private static Expr |
Ejp.compute(GuardedCmd g,
Expr normal,
Expr exceptional,
java.lang.String dynInstPrefix,
VarMap dynInstMap)
|
static Set |
ATarget.compute(GuardedCmd gc)
|
private static void |
ATarget.F(GuardedCmd g,
java.util.Hashtable in,
java.util.Hashtable[] out)
|
|
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 NEXT | FRAMES NO FRAMES |