Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## 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)`

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage