|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
IExpressionFactory interface,
with convenience implementations of several methods.ptr represents an allocated block of
storage of size bytes (used in source code annotations).
e
e
IBitVectorExpression.
IBooleanExpression.
IIntegerExpression.
IIntegerVariableExpression.
IRationalExpression.
IRationalVariableExpression.
rval to the memory location lval in pre-state
state.
E to lval x with precondition
P results in:
(∃ memory' : (∃ memory : P ∧ memory' = memory[x ↦ E]) ∧ memory = memory'),
where memory is an array representing the memory state and memory'
is a temporary to bridge the quantifier.
x:=E along path P results in:
if is_ok(P) then ok(〚x:=E〛(val(P))) else bottom
if is_ok(P) => 〚E〛(val(P)) then P else bottom
IUnaryFunctionExpression.
- asUnaryFunctionExpression(Expression<UnaryFunctionType<D, R>>) -
Method in interface edu.nyu.cascade.prover.ExpressionManager
-
- asUnaryFunctionType(Type<UnaryFunctionType<D, R>>) -
Method in interface edu.nyu.cascade.prover.ExpressionManager
-
- asVariable() -
Method in class edu.nyu.cascade.fds.impl.StateExpressionImpl
-
- asVariable() -
Method in interface edu.nyu.cascade.prover.Expression
- Coerce the expression to a
IVariableExpression.
- asVariable(Expression<T>) -
Method in interface edu.nyu.cascade.prover.ExpressionManager
-
- atPredicate(String, String...) -
Method in class edu.nyu.cascade.fds.DualStateExpressionFactory
-
- atPredicate(String, DualExpression<Int, Bool>) -
Method in class edu.nyu.cascade.fds.DualStateExpressionFactory
-
- atPredicate(DualExpression<Int, Bool>, String, String...) -
Method in class edu.nyu.cascade.fds.DualStateExpressionFactory
-
- atPredicate(String, String...) -
Method in class edu.nyu.cascade.fds.impl.StateExpressionFactoryImpl
-
- atPredicate(String, StateExpression<IntegerType>) -
Method in class edu.nyu.cascade.fds.impl.StateExpressionFactoryImpl
-
- atPredicate(StateExpression<IntegerType>, String, String...) -
Method in class edu.nyu.cascade.fds.impl.StateExpressionFactoryImpl
-
- atPredicate(String, String...) -
Method in interface edu.nyu.cascade.fds.StateExpressionFactory
- Retrieve an "at predicate" for a label in the CFG, given the name of the label.
- atPredicate(String, Int) -
Method in interface edu.nyu.cascade.fds.StateExpressionFactory
- Deprecated.
- atPredicate(Int, String, String...) -
Method in interface edu.nyu.cascade.fds.StateExpressionFactory
-
- await(Node, IRExpressionImpl) -
Static method in class edu.nyu.cascade.ir.impl.Statement
-
qName.
n mod 2size.
rep.
expr, according to the conversion rule of the underlying
encoding.
expr, according to the conversion rule of the underlying
encoding.
bool, according to the conversion rule of the underlying
encoding.
bool, according to the conversion rule of the underlying
encoding.
expr
minus one.
expr
minus one.
p.
e.
e.
lhs and
rhs for equality.
e.
e in state.
false.
ExpressionManager.forall(Iterable,Expression,Iterable)
NOTE: Concrete implementations of IBooleanType may ignore triggers.
Printer.
symbolTable, using base as a starting point.
namespace in
the current scope of the given symbolTable, using
base as a starting point.
name, with variable argument list args.
name, with variable argument list args.
name, with variable argument list args.
name, with variable argument list args.
e.
isValid() returns false, gives an
inconsistent set of assertions that are implied by the assumptions and the
formula.
IExpressionManager object used in the underlying
expression encoding.
IExpressionManager object used in the underlying
expression encoding.
IExpressionManager object used in the underlying
expression encoding.
null).
Expression.Kind).
block.
getResultType() returns SATISFIABLE, gives a
consistent set of sub-formulas which are sufficient to satisfy the last
formula under the given assumptions.
block.
Type).
lhs and
rhs.
lhs and
rhs.
e.
e.
e.
e
e
thenExpr if
bool holds and the value of elseExpr otherwise.
e
e
expression.
expression.
type.
expr
plus one.
expr
plus one.
a[i]) given an
array and an index value.
c.
id.
var
is bound as a parameter.
vars
are bound as parameters.
vars are bound as parameters.
var is bound as a parameter.
e.
lhs and
rhs.
lhs and
rhs.
file (see
Properties.load(java.io.InputStream)).
path (see
Properties.load(java.io.InputStream)).
url (see
Properties.load(java.io.InputStream)).
e.
e.
e.
e.
e.
e.
lhs and
rhs for disequality.
e.
Iterable disjuncts is true.
b.
e
e
e.
e.
e.
e.
edu.nyu.cascade.util.Preferences.
edu.nyu.cascade.util.Preferences.
location lies between
two basic blocks.
splitAt(location,true)
e in oldExprs for the corresponding expression e'
in newExprs.
oldExpr for newExpr in
e.
e.
__func__'s type for the function with the
specified name.
s.
true.
base as a starting point.
a[i <- e]) given
an array, an index value, and an element value.
e
e
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||