|
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 |
java.lang.Objectescjava.backpred.BackPred
Generates the background predicate for a given type.
The background predicate for a particular class or
interface type T consists of the conjunction of the background
predicates contributions of each contributor class. See
FindContributors
for the definition of the
contributors of a class.
A type must be typechecked in order to generate its background predicate. A type need only be prepped in order to generate its background predicate contribution.
Constructor Summary | |
BackPred()
|
Method Summary | |
protected static void |
addContribution(TypeDecl d,
java.io.PrintStream proverStream)
Add to b the contribution from a particular TypeDecl, which is a formula. |
protected static void |
bg(java.lang.String s,
java.io.PrintStream proverStream)
Called with a simplify command. |
protected static void |
bgi(java.lang.String s,
java.io.PrintStream proverStream)
Called with an S-expression that may contain a free variable "t". |
protected static Expr |
eq(Expr e1,
Expr e2,
Type t)
Generate the appropriate GC equality e1 == e2 based on type t. |
protected static LiteralExpr |
eval(Expr e,
int loc)
Like ConstantExpr.eval, but returns a LiteralExpr instead of an Integer/Long/etc. |
private static void |
genFinalInitInfo(VarInit initExpr,
GenericVarDecl sDecl,
Expr s,
Expr x,
Type type,
int loc,
java.io.PrintStream proverStream)
|
static void |
genTypeBackPred(FindContributors scope,
java.io.PrintStream proverStream)
Return the type-specific background predicate as a formula. |
static void |
genUnivBackPred(java.io.PrintStream proverStream)
Returns the universal background predicate as a sequence of simplify commands. |
protected static boolean |
isStaticallyNonNull(VarInit e)
Do we know statically that an expression always returns a non-null value? |
private static void |
produce(GenericVarDecl sDecl,
Expr s,
Expr e,
java.io.PrintStream proverStream)
|
private static void |
sayIsFinal(Type x,
java.io.PrintStream proverStream)
Record in the background predicate that x is final. |
private static void |
saySubClass(Type x,
Type y,
java.io.PrintStream proverStream)
Record in the background predicate that x is a subclass of y. |
private static void |
saySubType(Type x,
Type y,
java.io.PrintStream proverStream)
Record in the background predicate that x is a subtype of y. |
private static void |
saySuper(TypeDecl d,
java.io.PrintStream proverStream)
|
static java.lang.String |
simplifyTypeName(Type x)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
public BackPred()
Method Detail |
public static void genUnivBackPred(java.io.PrintStream proverStream)
public static void genTypeBackPred(FindContributors scope, java.io.PrintStream proverStream)
private static void genFinalInitInfo(VarInit initExpr, GenericVarDecl sDecl, Expr s, Expr x, Type type, int loc, java.io.PrintStream proverStream)
private static void produce(GenericVarDecl sDecl, Expr s, Expr e, java.io.PrintStream proverStream)
protected static void addContribution(TypeDecl d, java.io.PrintStream proverStream)
private static void saySubClass(Type x, Type y, java.io.PrintStream proverStream)
private static void saySubType(Type x, Type y, java.io.PrintStream proverStream)
private static void saySuper(TypeDecl d, java.io.PrintStream proverStream)
private static void sayIsFinal(Type x, java.io.PrintStream proverStream)
public static java.lang.String simplifyTypeName(Type x)
protected static void bgi(java.lang.String s, java.io.PrintStream proverStream)
protected static void bg(java.lang.String s, java.io.PrintStream proverStream)
protected static boolean isStaticallyNonNull(VarInit e)
protected static LiteralExpr eval(Expr e, int loc)
Ignores String constants. (Always returns null in that case.)
If returns a non-null LiteralExpr, sets its loc to
loc
.
protected static Expr eq(Expr e1, Expr e2, Type t)
|
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 |