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.pa
Class PredicateAbstraction

java.lang.Object
  extended byescjava.pa.PredicateAbstraction

public class PredicateAbstraction
extends java.lang.Object


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

paDecoration

public static ASTDecoration paDecoration

quantifyAssumptions

private static boolean quantifyAssumptions

invariants

ExprVec invariants

bddManager

private mocha.wrappers.jbdd.jbddManager bddManager

abstractor

public Abstractor abstractor

skolemConstants

private LocalVarDeclVec skolemConstants

loopPredicates

private ExprVec loopPredicates

body

private GuardedCmd body

bodyDesugared

private GuardedCmd bodyDesugared

havoc

private GuardedCmd havoc

startLoc

private int startLoc

nQueries

public int nQueries

milliSecsUsed

long milliSecsUsed

perfCount

GCProver perfCount

code

private final StackVector code

temporaries

private final GenericVarDeclVec temporaries
Constructor Detail

PredicateAbstraction

PredicateAbstraction(LoopCmd g,
                     Set env)
Method Detail

abstractLoop

static GuardedCmd abstractLoop(LoopCmd g,
                               GuardedCmd context,
                               Set env)

abstractLoopHelper

private GuardedCmd abstractLoopHelper(GuardedCmd context,
                                      Set env)

skolemQuantInvariants

public static ExprVec skolemQuantInvariants(LocalVarDeclVec skolemConstants,
                                            ExprVec invs,
                                            int sloc,
                                            int eloc)

mentions

private static boolean mentions(Expr e,
                                GenericVarDecl d)

inferPredicates

private void inferPredicates(LoopCmd g,
                             Set env,
                             Set targets)

guessPredicate

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

The ESC/Java2 Project Homepage