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 CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.translate
Class GC

    java.lang.Object
      escjava.translate.GC

public final class GC
extends java.lang.Object

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

### assertContinueCounter

    private static int assertContinueCounter

### nulllit

    public static final Expr nulllit

### zerolit

    public static final Expr zerolit

### onelit

    public static final Expr onelit

### truelit

    public static final Expr truelit

### falselit

    public static final Expr falselit

### dzerolit

    public static final Expr dzerolit

### allocvar

    public static final VariableAccess allocvar

### ecvar

    public static final VariableAccess ecvar

### elemsvar

    public static final VariableAccess elemsvar

### resultvar

    public static final VariableAccess resultvar

### xresultvar

    public static final VariableAccess xresultvar

### objectTBCvar

    public static final VariableAccess objectTBCvar

### statevar

    public static final VariableAccess statevar

### LSvar

    public static VariableAccess LSvar

### thisvar

    public static final VariableAccess thisvar

### ec_throw

    public static final Expr ec_throw

### ec_return

    public static final Expr ec_return

Constructor Detail

### GC

    public GC()

Method Detail

### block

    public static GuardedCmd block(GenericVarDeclVec v,
                                   GuardedCmd g)

### blockL

    public static GuardedCmd blockL(Stmt label,
                                    GuardedCmd g)

### seq

    public static GuardedCmd seq(GuardedCmd g1,
                                 GuardedCmd g2)

  Requires `0 < cmds.size()`.

### seq

    public static GuardedCmd seq(GuardedCmd g1,
                                 GuardedCmd g2,
                                 GuardedCmd g3)

### seq

    public static GuardedCmd seq(GuardedCmd g1,
                                 GuardedCmd g2,
                                 GuardedCmd g3,
                                 GuardedCmd g4)

### seq

    public static GuardedCmd seq(GuardedCmdVec cmds)

  May mutilate contents of `cmds`. The caller is expected not to use `cmds` after this call.

### gets

    public static GuardedCmd gets(VariableAccess lhs,
                                  Expr rhs)

### subgets

    public static GuardedCmd subgets(VariableAccess lhs,
                                     Expr index,
                                     Expr rhs)

### subsubgets

    public static GuardedCmd subsubgets(VariableAccess lhs,
                                        Expr array,
                                        Expr index,
                                        Expr rhs)

### restoreFrom

    public static GuardedCmd restoreFrom(VariableAccess lhs,
                                         Expr rhs)

### raise

    public static GuardedCmd raise()

### skip

    public static GuardedCmd skip()

### loop

    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)

### ifcmd

    public static GuardedCmd ifcmd(Expr t,
                                   GuardedCmd c,
                                   GuardedCmd a)

### boxPopFromStackVector

    public static GuardedCmd boxPopFromStackVector(StackVector s)

  Pops two command sequences off `s`, call them `a` and `b`. Then returns the box composition of these commands, that is, `a [] b`.

### choosecmd

    public static GuardedCmd choosecmd(GuardedCmd a,
                                       GuardedCmd b)

### trycmd

    public static GuardedCmd trycmd(GuardedCmd c,
                                    GuardedCmd a)

### isBooleanLiteral

    public static boolean isBooleanLiteral(Expr e,
                                           boolean b)

  Returns `true` when `e` is a boolean literal expression whose value is `b`.

### isFalse

    public static boolean isFalse(Expr e)

  Returns `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.

### check

    public 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. There are two versions of the `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`.

### check

    public static GuardedCmd check(int locUse,
                                   int errorName,
                                   Expr pred,
                                   int locPragmaDecl,
                                   java.lang.Object aux)

### check

    public static GuardedCmd check(int locUse,
                                   int errorName,
                                   Expr pred,
                                   int locPragmaDecl,
                                   int auxLoc,
                                   java.lang.Object aux)

### check

    public static GuardedCmd check(int locUse,
                                   Condition cond)

  See description of `check` above.

### check

    public static GuardedCmd check(int locUse,
                                   Condition cond,
                                   java.lang.Object aux)

  See description of `check` above.

### condition

    public static Condition condition(int label,
                                      Expr pred,
                                      int locPragmaDecl)

### freeCondition

    public static Condition freeCondition(Expr pred,
                                          int locPragmaDecl)

### assumeCondition

    public static Condition assumeCondition(Expr pred,
                                            int locPragmaDecl)

### assumeAnnotation

    public static GuardedCmd assumeAnnotation(int locPragmaDecl,
                                              Expr p)

### assume

    public static GuardedCmd assume(Expr p)

### assumeNegation

    public static GuardedCmd assumeNegation(Expr p)

### fail

    public static GuardedCmd fail()

### assertPredicate

    private static GuardedCmd assertPredicate(int locUse,
                                              int errorName,
                                              Expr pred,
                                              int locPragmaDecl,
                                              int auxLoc,
                                              java.lang.Object aux)

### makeLabel

    public static Identifier makeLabel(java.lang.String name,
                                       int locPragmaDecl,
                                       int auxLoc,
                                       int locUse)

### makeLabel

    public static Identifier makeLabel(java.lang.String name,
                                       int locPragmaDecl,
                                       int locUse)

### makeFullLabel

    public static Identifier makeFullLabel(java.lang.String name,
                                           int locPragmaDecl,
                                           int locUse)

### subst

    public static Expr subst(int sloc,
                             int eloc,
                             java.util.Hashtable subst,
                             Expr target)

### subst

    public static Expr subst(int sloc,
                             int eloc,
                             GenericVarDecl var,
                             Expr val,
                             Expr target)

### subst

    public static Expr subst(GenericVarDecl var,
                             Expr val,
                             Expr target)

### symlit

    public static Expr symlit(java.lang.String s)

### symlit

    public static Expr symlit(Stmt s,
                              java.lang.String prefix)

### zeroequiv

    public static Expr zeroequiv(Type t)

### makeVar

    public static VariableAccess makeVar(Identifier name,
                                         int locId)

### makeVar

    public static VariableAccess makeVar(java.lang.String name,
                                         int locId)

### makeFormalPara

    public static VariableAccess makeFormalPara(java.lang.String name,
                                                Type type,
                                                int locId)

### makeVar

    public static VariableAccess makeVar(java.lang.String name)

### makeVar

    public static VariableAccess makeVar(Identifier name)

### makeFormalPara

    public static VariableAccess makeFormalPara(java.lang.String name,
                                                Type type)

### makeFormalPara

    public static VariableAccess makeFormalPara(java.lang.String name)

### typeExpr

    public static Expr typeExpr(Type t)

### cast

    public static Expr cast(Expr e,
                            Type t)

### nary

    public static Expr nary(int tag,
                            Expr e)

### nary

    public static Expr nary(int sloc,
                            int eloc,
                            int tag,
                            Expr e)

### nary

    public static Expr nary(int tag,
                            Expr e1,
                            Expr e2)

### nary

    public static Expr nary(int sloc,
                            int eloc,
                            int tag,
                            Expr e1,
                            Expr e2)

### nary

    public static Expr nary(int tag,
                            Expr e1,
                            Expr e2,
                            Expr e3)

### nary

    public static Expr nary(int sloc,
                            int eloc,
                            int tag,
                            Expr e1,
                            Expr e2,
                            Expr e3)

### nary

    public static Expr nary(int tag,
                            ExprVec ev)

### nary

    public static Expr nary(Identifier id,
                            ExprVec ev)

### nary

    public static Expr nary(Identifier id,
                            Expr e)

### nary

    public static Expr nary(Identifier id,
                            Expr e1,
                            Expr e2)

### nary

    public static Expr nary(int sloc,
                            int eloc,
                            Identifier id,
                            ExprVec ev)

### nary

    public static Expr nary(int sloc,
                            int eloc,
                            int tag,
                            ExprVec ev)

### select

    public static Expr select(Expr c0,
                              Expr c1)

### not

    public static Expr not(Expr c)

### not

    public static Expr not(int sloc,
                           int eloc,
                           Expr c)

### and

    public static Expr and(Expr c1,
                           Expr c2)

### andx

    public static Expr andx(Expr c1,
                            Expr c2)

### and

    public static Expr and(int sloc,
                           int eloc,
                           Expr c1,
                           Expr c2)

### and

    public static Expr and(ExprVec v)

### and

    public static Expr and(int sloc,
                           int eloc,
                           ExprVec v)

### or

    public static Expr or(Expr c1,
                          Expr c2)

### or

    public static Expr or(int sloc,
                          int eloc,
                          Expr c1,
                          Expr c2)

### or

    public static Expr or(ExprVec v)

### or

    public static Expr or(int sloc,
                          int eloc,
                          ExprVec v)

### implies

    public static Expr implies(Expr c0,
                               Expr c1)

### implies

    public static Expr implies(int sloc,
                               int eloc,
                               Expr c0,
                               Expr c1)

### forall

    public static Expr forall(GenericVarDecl v,
                              Expr e)

### forall

    public static Expr forall(GenericVarDecl v,
                              Expr range,
                              Expr e)

### forall

    public static Expr forall(GenericVarDeclVec v,
                              Expr range,
                              Expr e)

### forall

    public static Expr forall(GenericVarDecl v,
                              Expr e,
                              ExprVec nopats)

### forallwithpats

    public static Expr forallwithpats(GenericVarDecl v,
                                      Expr e,
                                      ExprVec pats)

### forall

    public static Expr forall(int sloc,
                              int eloc,
                              GenericVarDecl v,
                              Expr range,
                              Expr e)

### forall

    public static Expr forall(int sloc,
                              int eloc,
                              GenericVarDecl v,
                              Expr range,
                              Expr e,
                              ExprVec nopats)

### quantifiedExpr

    public static Expr quantifiedExpr(int sloc,
                                      int eloc,
                                      int tag,
                                      GenericVarDecl v,
                                      Expr range,
                                      Expr e,
                                      ExprVec nopats,
                                      ExprVec pats)

### quantifiedExpr

    public static Expr quantifiedExpr(int sloc,
                                      int eloc,
                                      int tag,
                                      GenericVarDeclVec vs,
                                      Expr range,
                                      Expr e,
                                      ExprVec nopats,
                                      ExprVec pats)

### isSimple

    public static boolean isSimple(Expr e)

### selectiveAdd

    private static boolean selectiveAdd(ExprVec to,
                                        ExprVec from,
                                        Expr bot,
                                        Expr top,
                                        int naryTagMerge)

  Adds elements to `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.

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 CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage