---

PredicateSet Class Reference

List of all members.

Public Methods
void	addValuePredicate (String name, Expr expr)
Vector	getValuePredicates ()
boolean	isObservable (Object o)
String	predicateName (Object pred)
void	print ()
	PredicateSet (Name name)
Name	getName ()
java util Hashtable	getPredicateTable ()
void	putPredicate (Predicate predicate) throws DuplicatePredicateException
Static Public Methods
TreeSet	getDefinedPredicates (Object key)
Predicate	getPredicate (Name name) throws PredicateNotDeclaredException
PredicateSet	getPredicateSet (Name name) throws PredicateSetNotDeclaredException
Hashtable	getPredicateSetTable ()
void	reset ()
Private Methods
void	addPredicateLocation (Stmt stmt, Location loc)
LocVector	getPredicateLocations (Stmt stmt)
Static Private Methods
void	putPredicateSet (PredicateSet predicateSet)
Private Attributes
Vector	valuePredicates = new Vector()
Hashtable	predicateName = new Hashtable()
Hashtable	predLocations = new Hashtable()
Hashtable	observableSet = new Hashtable()
Name	name
Hashtable	predTable = new Hashtable()
Static Private Attributes
Hashtable	table = new Hashtable()
Hashtable	defTable = new Hashtable()

---

Detailed Description

PredicateSet allows the caller of BIRC to define state predicates that will appear in the translator input.

Predicates on the location of threads should be specified as value predicates using the LocationTestExpr extension to Jimple.

Usage:

 PredicateSet predicates = new PredicateSet(); 
 Vector stmts = new Vector(); 
 Stmt retStmt = ...; 
 stmt.addElement(retStmt); 
 LocationTestExpr test = new LocationTestExpr(stmts); 
 predicates.addValuePredicate("atReturn",test); 
 Expr xGT0Expr = ...; 
 predicates.addValuePredicate("xGT0",xGT0Expr); 
 

Definition at line 65 of file birc/PredicateSet.java.

---

Constructor & Destructor Documentation

PredicateSet::PredicateSet (  Name   name )  [inline]

Parameters: name   edu.ksu.cis.bandera.jjjc.symboltable.Name Definition at line 50 of file specification/predicate/datastructure/PredicateSet.java.

---

Member Function Documentation

void PredicateSet::addValuePredicate (  String   name, Expr   expr )  [inline]

Add a value predicate (a Jimple Expr) Parameters: name   name of predicate expr   Jimple Expr specifying condition when predicate is true Definition at line 87 of file birc/PredicateSet.java.

TreeSet PredicateSet::getDefinedPredicates (  Object   key )  [inline, static]

Returns: java.util.TreeSet Parameters: key   java.lang.Object Definition at line 59 of file specification/predicate/datastructure/PredicateSet.java.

Name PredicateSet::getName (    )  [inline]

Returns: edu.ksu.cis.bandera.jjjc.symboltable.Name Definition at line 70 of file specification/predicate/datastructure/PredicateSet.java. Referenced by putPredicateSet().

Predicate PredicateSet::getPredicate (  Name   name )  [inline, static]

Returns: edu.ksu.cis.bandera.predicate.datastructure.Predicate Parameters: name   edu.ksu.cis.bandera.jjjc.symboltable.Name Definition at line 78 of file specification/predicate/datastructure/PredicateSet.java.

PredicateSet PredicateSet::getPredicateSet (  Name   name )  [inline, static]

Returns: edu.ksu.cis.bandera.predicate.datastructure.PredicateSet Parameters: name   edu.ksu.cis.bandera.jjjc.symboltable.Name Definition at line 94 of file specification/predicate/datastructure/PredicateSet.java. Referenced by getPredicate().

Hashtable PredicateSet::getPredicateSetTable (    )  [inline, static]

Returns: java.util.Hashtable Definition at line 104 of file specification/predicate/datastructure/PredicateSet.java.

java util Hashtable PredicateSet::getPredicateTable (    )  [inline]

Returns: java.util.Hashtable Definition at line 111 of file specification/predicate/datastructure/PredicateSet.java.

void PredicateSet::putPredicate (  Predicate   predicate )  [inline]

Parameters: predicate   edu.ksu.cis.bandera.predicate.datastructure.Predicate Definition at line 118 of file specification/predicate/datastructure/PredicateSet.java.

void PredicateSet::putPredicateSet (  PredicateSet   predicateSet )  [inline, static, private]

Parameters: predicateSet   edu.ksu.cis.bandera.predicate.datastructure.PredicateSet Definition at line 145 of file specification/predicate/datastructure/PredicateSet.java.

---

The documentation for this class was generated from the following files:

• birc/PredicateSet.java
• specification/predicate/datastructure/PredicateSet.java

---