|
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.pa.PredicateAbstraction
Field Summary | |
Abstractor |
abstractor
|
private mocha.wrappers.jbdd.jbddManager |
bddManager
|
private GuardedCmd |
body
|
private GuardedCmd |
bodyDesugared
|
private StackVector |
code
|
private GuardedCmd |
havoc
|
(package private) ExprVec |
invariants
|
private ExprVec |
loopPredicates
|
(package private) long |
milliSecsUsed
|
int |
nQueries
|
static ASTDecoration |
paDecoration
|
(package private) GCProver |
perfCount
|
private static boolean |
quantifyAssumptions
|
private LocalVarDeclVec |
skolemConstants
|
private int |
startLoc
|
private GenericVarDeclVec |
temporaries
|
Constructor Summary | |
(package private) |
PredicateAbstraction(LoopCmd g,
Set env)
|
Method Summary | |
(package private) static GuardedCmd |
abstractLoop(LoopCmd g,
GuardedCmd context,
Set env)
|
private GuardedCmd |
abstractLoopHelper(GuardedCmd context,
Set env)
|
private void |
guessPredicate(Expr e,
Expr eOld,
Type type,
ExprVec predicates,
int loc,
Expr sca,
ExprVec boundsSC)
|
private void |
inferPredicates(LoopCmd g,
Set env,
Set targets)
|
private static boolean |
mentions(Expr e,
GenericVarDecl d)
|
static ExprVec |
skolemQuantInvariants(LocalVarDeclVec skolemConstants,
ExprVec invs,
int sloc,
int eloc)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static ASTDecoration paDecoration
private static boolean quantifyAssumptions
ExprVec invariants
private mocha.wrappers.jbdd.jbddManager bddManager
public Abstractor abstractor
private LocalVarDeclVec skolemConstants
private ExprVec loopPredicates
private GuardedCmd body
private GuardedCmd bodyDesugared
private GuardedCmd havoc
private int startLoc
public int nQueries
long milliSecsUsed
GCProver perfCount
private final StackVector code
private final GenericVarDeclVec temporaries
Constructor Detail |
PredicateAbstraction(LoopCmd g, Set env)
Method Detail |
static GuardedCmd abstractLoop(LoopCmd g, GuardedCmd context, Set env)
private GuardedCmd abstractLoopHelper(GuardedCmd context, Set env)
public static ExprVec skolemQuantInvariants(LocalVarDeclVec skolemConstants, ExprVec invs, int sloc, int eloc)
private static boolean mentions(Expr e, GenericVarDecl d)
private void inferPredicates(LoopCmd g, Set env, Set targets)
private void guessPredicate(Expr e, Expr eOld, Type type, ExprVec predicates, int loc, Expr sca, ExprVec boundsSC)
|
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 |