Uses of Class
dev.civl.mc.semantics.IF.Evaluation

Packages that use Evaluation

Package	Description
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.

Uses of Evaluation in dev.civl.mc.semantics.IF

Methods in dev.civl.mc.semantics.IF that return Evaluation

Modifier and Type	Method	Description
Evaluation	Evaluator.dereference(CIVLSource source, State state, int pid, String process, dev.civl.sarl.IF.expr.SymbolicExpression pointer, boolean checkedOutput, boolean strict)	Given a pointer value, dereferences it in the given state to yield the symbolic expression value stored at the referenced location.
Evaluation	Evaluator.evaluate(State state, int pid, Expression expression)
Evaluation	Evaluator.evaluate(State state, int pid, Expression expression, boolean checkUndefinedValue)	Evaluates the expression and returns the result, which is a symbolic expression value.
Evaluation	Evaluator.evaluateCastWorker(State state, int pid, String process, CIVLType castType, Expression arg)
Evaluation	LibraryEvaluator.evaluateGuard(CIVLSource source, State state, int pid, String function, Expression[] arguments)	Evaluates the guard of a system function.
Evaluation	Evaluator.evaluatePointerAdd(State state, int pid, BinaryExpression expression, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression offset)	Evaluates pointer addition.
Evaluation	Evaluator.evaluateSizeofType(CIVLSource source, State state, int pid, CIVLType type)	Evaluate the size of a CIVL type.
Evaluation	LibraryExecutor.execute(State state, int pid, CallOrSpawnStatement statement, String functionName)	Executes the given call statement for a certain process at the given state.
Evaluation	Executor.execute_printf(CIVLSource source, State state, int pid, String process, Expression[] arguments, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues, boolean forcePrint)
Evaluation	Evaluator.getStringExpression(State state, int pid, String process, CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression charPointer)	Given a pointer to char, returns the symbolic expression of type array of char which is the string pointed to.
Evaluation	Evaluator.havoc(State state, dev.civl.sarl.IF.type.SymbolicType type)	returns an arbitrary symbolic constant with the given type.
Evaluation	Evaluator.initialValueOfType(State state, int pid, CIVLType type)	Given a CIVLType t, returns the default initial value of an object of t as if the object has static storage.
Evaluation	Executor.malloc(CIVLSource source, State state, int pid, String process, Expression scopeExpression, dev.civl.sarl.IF.expr.SymbolicExpression scopeValue, CIVLType objectType, dev.civl.sarl.IF.expr.SymbolicExpression objectValue)	Adds a new object to the heap of a certain scope; returns the pointer of the object in the heap.
Evaluation	Evaluator.pointerSubtraction(State state, int pid, String process, BinaryExpression expression, dev.civl.sarl.IF.expr.SymbolicExpression leftPtr, dev.civl.sarl.IF.expr.SymbolicExpression rightPtr)	Evaluation pointer subtraction.
Evaluation	Evaluator.reference(State state, int pid, LHSExpression operand)	Creates a pointer value by evaluating a left-hand-side expression in the given state.

Methods in dev.civl.mc.semantics.IF that return types with arguments of type Evaluation

Modifier and Type	Method	Description
Pair<Evaluation,dev.civl.sarl.IF.expr.NumericExpression[]>	Evaluator.arrayElementReferenceAdd(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression ptr, dev.civl.sarl.IF.expr.NumericExpression offset, CIVLSource source)	Do a pointer addition operation on the given pointer with the given offset.