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

Uses of Class
escjava.ast.GuardedCmd

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

The ESC/Java2 Project Homepage