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

escjava.translate
Class GC

java.lang.Object
  extended byescjava.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.


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