Uses of Interface
dev.civl.mc.model.IF.expression.Expression

Packages that use Expression

Package	Description
dev.civl.mc.model.IF	Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
dev.civl.mc.model.IF.contract
dev.civl.mc.model.IF.expression	Submodule model.expression defines expression in CIVL.
dev.civl.mc.model.IF.expression.reference
dev.civl.mc.model.IF.location	Submodule model.location defines a location in the control flow graph of CIVL.
dev.civl.mc.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.model.IF.type	Submodule model.type defines types in CIVL.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.

Uses of Expression in dev.civl.mc.model.IF

Methods in dev.civl.mc.model.IF that return Expression

Modifier and Type	Method	Description
Expression	ModelFactory.arithmeticableExpression(Expression expression)	Translates an expression to be of the type for arithmetic operations i.e.
Expression	ModelFactory.booleanExpression(Expression expression)	Convert an expression to be of boolean-type.
Expression	ModelFactory.comparableExpression(Expression expression)	Translates an expression to be of the type for comparable operations i.e.
Expression	LogicFunction.definition()
Expression	ModelFactory.functionGuardExpression(CIVLSource source, Expression function, List<Expression> arguments)
Expression	ModelFactory.nullPointerExpression(CIVLPointerType pointerType, CIVLSource source)	Generate a null pointer expression
Expression	ModelFactory.numericExpression(Expression expression)	Translates an expression to be of numeric-type (i.e., int or real).
Expression	ModelFactory.systemGuardExpression(CallOrSpawnStatement sysCall)	Creates the system guard expression for the given system call statement.
Expression	ModelFactory.trueExpression(CIVLSource source)	creates a new boolean expression which has the value $true

Methods in dev.civl.mc.model.IF that return types with arguments of type Expression

Modifier and Type	Method	Description
List<Pair<Expression,Integer>>	CIVLFunction.getPossibleValidConsequences()	Possible valid consequence is a valid contract expression which is POSSIBLE a consequence of the whole contract Notice that consequences only come from requirements

Methods in dev.civl.mc.model.IF with parameters of type Expression

Modifier and Type	Method	Description
Fragment	AccuracyAssumptionBuilder.accuracyAssumptions(Expression assumption, Scope scope)	Analyze an assumption.
void	Fragment.addGuardToStartLocation(Expression guard, ModelFactory factory)	Add a specified guard to the all statements of the start location.
Expression	ModelFactory.arithmeticableExpression(Expression expression)	Translates an expression to be of the type for arithmetic operations i.e.
ArrayLambdaExpression	ModelFactory.arrayLambdaExpression(CIVLSource source, CIVLArrayType arrayType, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new array lambda expression.
ArraySliceReference	ModelFactory.arraySliceReference(ArraySliceReference.ArraySliceKind sliceKind, Expression index)	creates a new array slice reference.
AssignStatement	ModelFactory.assignStatement(CIVLSource civlSource, Location source, LHSExpression lhs, Expression rhs, boolean isInitializer)	An assignment statement.
BinaryExpression	ModelFactory.binaryExpression(CIVLSource source, BinaryExpression.BINARY_OPERATOR operator, Expression left, Expression right)	A binary expression.
Expression	ModelFactory.booleanExpression(Expression expression)	Convert an expression to be of boolean-type.
CallOrSpawnStatement	ModelFactory.callOrSpawnStatement(CIVLSource sourceOf, Location location, boolean isCall, Expression function, List<Expression> arguments, Expression guard, boolean isInitializer)	Creates a call or spawn statement.
CastExpression	ModelFactory.castExpression(CIVLSource source, CIVLType type, Expression expression)	Create a cast expression
Fragment	ModelFactory.civlForEnterFragment(CIVLSource source, Location src, Expression dom, List<Variable> variables, Variable counter)	Returns a new fragment containing a CivlForStatement.
CivlParForSpawnStatement	ModelFactory.civlParForEnterStatement(CIVLSource source, Location location, Expression domain, VariableExpression domSize, VariableExpression procsVar, CIVLFunction parProcFunc)	creates a $parfor enter statement to start the execution of the $parfor.
Expression	ModelFactory.comparableExpression(Expression expression)	Translates an expression to be of the type for comparable operations i.e.
CIVLCompleteArrayType	CIVLTypeFactory.completeArrayType(CIVLType elementType, Expression extent)	Returns a new complete array type with specified extent (length expression) and element type.
ConditionalExpression	ModelFactory.conditionalExpression(CIVLSource source, Expression condition, Expression trueBranch, Expression falseBranch)	The ternary conditional expression ("?" in C).
DereferenceExpression	ModelFactory.dereferenceExpression(CIVLSource source, Expression pointer)	Returns a new dereference expression (*p) with operand pointer.
DifferentiableExpression	ModelFactory.differentiableExpression(CIVLSource source, AbstractFunction function, int degree, Expression[] lowerBounds, Expression[] upperBounds)	An expression representing the claim that some function is differentiable.
DomainGuardExpression	ModelFactory.domainGuard(CIVLSource source, List<Variable> vars, Variable counter, Expression domain)	Returns a domain guard expression which is boolean expression whose arguments consists of loop variables in a CIVL $for loop and the original domain associate to the loop.
DotExpression	ModelFactory.dotExpression(CIVLSource source, Expression struct, int fieldIndex)	A dot expression is a reference to a struct field.
ExtendedQuantifiedExpression	ModelFactory.extendedQuantifiedExpression(CIVLSource source, CIVLType type, dev.civl.abc.ast.node.IF.acsl.ExtendedQuantifiedExpressionNode.ExtendedQuantifier quant, Expression lo, Expression hi, Expression function)
Expression	ModelFactory.functionGuardExpression(CIVLSource source, Expression function, List<Expression> arguments)
NoopStatement	ModelFactory.ifElseBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isIf)	An if-else branch statement is introduced to translate if-else statement.
boolean	ModelFactory.isTrue(Expression expression)	Check if a certain expression is TRUE.
LambdaExpression	ModelFactory.lambdaExpression(CIVLSource source, CIVLFunctionType functionType, Variable variable, Expression expression)	Creates a new lambda expression.
LogicFunction	ModelFactory.logicFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType outputType, int[] pointerToHeapMap, Scope containingScope, Expression definition)	Create a new logic function (LogicFunction).
NoopStatement	ModelFactory.loopBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isTrue, LoopContract loopContract)	An loop branch statement is introduced when translating a loop.
MallocStatement	ModelFactory.mallocStatement(CIVLSource civlSource, Location source, LHSExpression lhs, CIVLType staticElementType, Expression scopeExpression, Expression sizeExpression, int mallocId, Expression guard)	Create a new malloc statement
NoopStatement	ModelFactory.noopStatement(CIVLSource civlSource, Location source, Expression expression)	A noop statement with the default guard of true.
NoopStatement	ModelFactory.noopStatementWtGuard(CIVLSource civlSource, Location source, Expression guard)	A noop statement with an explicit guard expression.
Expression	ModelFactory.numericExpression(Expression expression)	Translates an expression to be of numeric-type (i.e., int or real).
QuantifiedExpression	ModelFactory.quantifiedExpression(CIVLSource source, QuantifiedExpression.Quantifier quantifier, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new quantified expression.
RegularRangeExpression	ModelFactory.regularRangeExpression(CIVLSource source, Expression low, Expression high, Expression step)	Creates a regular range expression, which has the syntax low ..
Fragment	ModelFactory.returnFragment(CIVLSource civlSource, Location source, Expression expression, CIVLFunction function)	Create a one-statement fragment that contains the return statement.
SizeofExpression	ModelFactory.sizeofExpressionExpression(CIVLSource source, Expression argument)	Returns a new expression of the form "sizeof(e)" where is an expression.
SubscriptExpression	ModelFactory.subscriptExpression(CIVLSource source, LHSExpression array, Expression index)	An expression for an array index operation.
NoopStatement	ModelFactory.switchBranchStatement(CIVLSource civlSource, Location source, Expression guard)	Creates a switch branch statement for the default case, which is a subclass of no-op statement.
NoopStatement	ModelFactory.switchBranchStatement(CIVLSource civlSource, Location source, Expression guard, Expression label)	Creates a switch branch statement for a labeled case.
UnaryExpression	ModelFactory.unaryExpression(CIVLSource source, UnaryExpression.UNARY_OPERATOR operator, Expression operand)	A unary expression.
UpdateStatement	ModelFactory.updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CIVLFunction function, Expression[] arguments)
UpdateStatement	ModelFactory.updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CallOrSpawnStatement call)	Creates an $update statement.

Method parameters in dev.civl.mc.model.IF with type arguments of type Expression

Modifier and Type	Method	Description
AbstractFunctionCallExpression	ModelFactory.abstractFunctionCallExpression(CIVLSource source, AbstractFunction function, List<Expression> arguments)	An expression for a call to an abstract function.
void	CIVLFunction.addPossibleValidConsequence(Pair<Expression,Integer> validConsequences)	Possible valid consequence is a valid contract expression which is POSSIBLE a consequence of the whole contract Notice that consequences only come from requirements
ArrayLambdaExpression	ModelFactory.arrayLambdaExpression(CIVLSource source, CIVLArrayType arrayType, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new array lambda expression.
CallOrSpawnStatement	ModelFactory.callOrSpawnStatement(CIVLSource sourceOf, Location location, boolean isCall, Expression function, List<Expression> arguments, Expression guard, boolean isInitializer)	Creates a call or spawn statement.
Expression	ModelFactory.functionGuardExpression(CIVLSource source, Expression function, List<Expression> arguments)
LoopContract	ModelFactory.loopContract(CIVLSource civlSource, Location loopLocation, List<Expression> loopInvariants, List<LHSExpression> loopAssigns, List<Expression> loopVariants)	Creates a LoopContract instance
ParallelAssignStatement	ModelFactory.parallelAssignStatement(CIVLSource source, List<Pair<LHSExpression,Expression>> assignPairs)
QuantifiedExpression	ModelFactory.quantifiedExpression(CIVLSource source, QuantifiedExpression.Quantifier quantifier, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new quantified expression.
RecDomainLiteralExpression	ModelFactory.recDomainLiteralExpression(CIVLSource source, List<Expression> ranges, CIVLType type)	Create a rectangular domain expression, which has the form {r1, r2, ..., rm}, where m is the dimension of the domain, and ri (where 1 invalid input: '<'= i invalid input: '<'= m) is a range expression (either regular range or literal range).

Uses of Expression in dev.civl.mc.model.IF.contract

Methods in dev.civl.mc.model.IF.contract that return Expression

Modifier and Type	Method	Description
Expression	NamedFunctionBehavior.assumptions()	Returns the conjunction of all assumptions of this behavior.
Expression	FunctionContract.guard()	Returns the guard of the function.
Expression[]	LoopContract.loopInvariants()	Returns an array of loop invariants specified for this loop.
Expression[]	LoopContract.loopVariants()	Returns an array of loop variants specified for this loop.

Methods in dev.civl.mc.model.IF.contract that return types with arguments of type Expression

Modifier and Type	Method	Description
List<Expression>	CallEvent.arguments()	Returns the arguments of the call event.
Iterable<Expression>	FunctionBehavior.assignsMemoryUnits()	Returns the assigns clause of this behavior.
Iterable<Expression>	FunctionBehavior.ensurances()	Returns the postconditions of this behavior.
Set<Expression>	FunctionBehavior.getWaitsforList()	Get an iterable collection of expressions which contains arguments of a "waitsfor" clause.
Set<Expression>	MemoryEvent.memoryUnits()	Returns the memory units associated with this event.
Iterable<Expression>	FunctionBehavior.readsMemoryUnits()	Returns the reads clause of this behavior.
Iterable<Expression>	FunctionBehavior.requirements()	Returns the preconditions of this behavior.

Methods in dev.civl.mc.model.IF.contract with parameters of type Expression

Modifier and Type	Method	Description
void	FunctionBehavior.addAssignsMemoryUnit(Expression mu)	Add an assigns clause to this behavior.
void	FunctionBehavior.addPostcondition(Expression condition)	Returns the post condition of this behavior.
void	FunctionBehavior.addPrecondition(Expression condition)	Returns the precondition of this behavior.
void	FunctionBehavior.addReadsMemoryUnit(Expression mu)	Add a reads clause to this behavior.
void	NamedFunctionBehavior.setAssumption(Expression assumption)	Set the conjunction of all assumptions to this behavior.
void	FunctionContract.setGuard(Expression expression)	Sets the guard of the function.

Method parameters in dev.civl.mc.model.IF.contract with type arguments of type Expression

Modifier and Type	Method	Description
CallEvent	ContractFactory.newCallEvent(CIVLSource source, CIVLFunction function, List<Expression> arguments)	Creates a new instance of call event.
MemoryEvent	ContractFactory.newMemoryEvent(CIVLSource source, DependsEvent.DependsEventKind kind, Set<Expression> memoryUnits)	Creates a new instance of memory event of the given kind.
void	FunctionBehavior.setWaitsforList(Iterable<Expression> waitsforArgs)	Set an expression collection as the arguments set as the "waitsfor" clause.

Uses of Expression in dev.civl.mc.model.IF.expression

Subinterfaces of Expression in dev.civl.mc.model.IF.expression

Modifier and Type	Interface	Description
interface	AbstractFunctionCallExpression	An expression representing a call of an abstract function.
interface	AddressOfExpression	This represents an address-of expression, which contains one operand, and has the format: invalid input: '&x', where invalid input: '&' is the address-of operator and x is the operand.
interface	ArrayLambdaExpression	A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.
interface	BinaryExpression	A binary operation.
interface	BooleanLiteralExpression	A literal boolean value.
interface	BoundVariableExpression	A bound variable is a variable used in a quantified expression.
interface	CastExpression	A cast of an expression to a different type.
interface	CharLiteralExpression
interface	CompoundLiteralExpression	This class represents compound literal expressions, including string literals.
interface	ConditionalExpression	The ternary conditional expression ("?" in C).
interface	DereferenceExpression
interface	DerivativeCallExpression	An uninterpreted call to the derivative of an abstract function.
interface	DifferentiableExpression	This expression encodes the claim that a real, abstract function is differentiable.
interface	DomainGuardExpression	This is the guard expression of CIVL for loops ($for).
interface	DotExpression	A dot expression is a reference to a field in a struct or union.
interface	DynamicTypeOfExpression	A "DynamicTypeOf" expression.
interface	ExtendedQuantifiedExpression	The representation for the "fold expression" in ACSL, e.g.
interface	FunctionCallExpression
interface	FunctionGuardExpression	A function guard expression is the guard expression of a function call with a function pointer.
interface	FunctionIdentifierExpression
interface	HereOrRootExpression
interface	InitialValueExpression	An expression yielding the initial value of a variable.
interface	IntegerLiteralExpression	An integer literal.
interface	LambdaExpression	A CIVL-C quanti, bound variable declaration list, (optional) restriction and expression.
interface	LHSExpression	A left-hand-side expression.
interface	LiteralExpression	The parent of all literal expressions.
interface	MemoryUnitExpression	A memory unit expression is an expression that represents (part of) the memory related to some variable.
interface	Nothing
interface	ProcnullExpression
interface	QuantifiedExpression	A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.
interface	RealLiteralExpression	A real literal.
interface	RecDomainLiteralExpression	This is a rectangular domain literal expression, which is the Cartesian product of a number of ranges, e.g., {range1, range2, range3, ...}.
interface	RegularRangeExpression	Represents a CIVL-C regular range expression, which has the form lo ..
interface	ScopeofExpression	A scopeof expression is "$scopeof(expr)".
interface	SelfExpression	Self expression.
interface	SizeofExpression	An expression of the form "sizeof(e)" where e is an expression.
interface	SizeofTypeExpression	An expression of the form "sizeof(t)" where t is a type.
interface	StatenullExpression	This class represents a $state_null constant expression.
interface	SubscriptExpression	a[i], where "a" is an array and "i" is an expression evaluating to an integer.
interface	SystemGuardExpression	A system guard expression is a pseudo guard expression for system function calls.
interface	UnaryExpression	A unary operation.
interface	UndefinedProcessExpression	Self expression.
interface	VariableExpression	A use of a variable in an expression.
interface	WildcardExpression	This represents the expression ..., which is used only in contracts and stands for an expression of any type whose value is ignored.

Methods in dev.civl.mc.model.IF.expression that return Expression

Modifier and Type	Method	Description
Expression	DomainGuardExpression.domain()	Returns the domain expression.
Expression	ArrayLambdaExpression.expression()	The expression e(x).
Expression	QuantifiedExpression.expression()	The expression e(x).
Expression	ExtendedQuantifiedExpression.function()	returns the function
Expression	FunctionGuardExpression.functionExpression()	Returns the function expression of the corresponding call statement of this guard expression.
Expression	SizeofExpression.getArgument()
Expression	ConditionalExpression.getCondition()
Expression	CastExpression.getExpression()
Expression	CompoundLiteralExpression.CIVLScalarLiteralObject.getExpression()
Expression	ConditionalExpression.getFalseBranch()
Expression	RegularRangeExpression.getHigh()	Returns the upper bound argument hi.
Expression	RegularRangeExpression.getLow()	Returns the lower bound argument lo.
Expression	RegularRangeExpression.getStep()	Returns the step argument step if it is present, else returns null
Expression	ConditionalExpression.getTrueBranch()
Expression	ExtendedQuantifiedExpression.higher()	returns the higher bound
Expression	SubscriptExpression.index()
Expression	LambdaExpression.lambdaFunction()	The expression e(x).
Expression	BinaryExpression.left()
Expression	ExtendedQuantifiedExpression.lower()	returns the lower bound
Expression[]	DifferentiableExpression.lowerBounds()	Gets the lower bounds of the intervals.
Expression	UnaryExpression.operand()
Expression	DereferenceExpression.pointer()	Returns the sole argument of this dereference expression.
Expression	RecDomainLiteralExpression.rangeAt(int index)	Returns the range expression of the domain literal at the given index.
Expression	Expression.replaceWith(ConditionalExpression oldExpression, Expression newExpression)	Attempt to create a expression by replacing a certain conditional expression with a new expression, used when translating away conditional expressions without introduction temporal variable
Expression	ArrayLambdaExpression.restriction()	Boolean-valued expression assumed to hold when evaluating expression.
Expression	QuantifiedExpression.restriction()	Boolean-valued expression assumed to hold when evaluating expression.
Expression	BinaryExpression.right()
Expression	DotExpression.structOrUnion()
Expression[]	DifferentiableExpression.upperBounds()	Gets the upper bounds of the intervals.

Methods in dev.civl.mc.model.IF.expression that return types with arguments of type Expression

Modifier and Type	Method	Description
List<Expression>	AbstractFunctionCallExpression.arguments()
List<Expression>	FunctionGuardExpression.arguments()	Returns the list of arguments of the corresponding function call statement.
List<Expression>	SystemGuardExpression.arguments()	The list of arguments that this function call uses.
List<Pair<List<Variable>,Expression>>	ArrayLambdaExpression.boundVariableList()	The list of bound variables.
List<Pair<List<Variable>,Expression>>	QuantifiedExpression.boundVariableList()	The list of bound variables.
List<Expression>	CompoundLiteralExpression.CIVLLiteralObject.subExpressions()

Methods in dev.civl.mc.model.IF.expression with parameters of type Expression

Modifier and Type	Method	Description
CompoundLiteralExpression.CIVLLiteralObject	CompoundLiteralExpression.createScalarLiteralObject(CIVLType type, Expression expr)
Expression	Expression.replaceWith(ConditionalExpression oldExpression, Expression newExpression)	Attempt to create a expression by replacing a certain conditional expression with a new expression, used when translating away conditional expressions without introduction temporal variable
void	SubscriptExpression.setIndex(Expression index)
void	UnaryExpression.setOperand(Expression operand)

Uses of Expression in dev.civl.mc.model.IF.expression.reference

Methods in dev.civl.mc.model.IF.expression.reference that return Expression

Modifier and Type	Method	Description
Expression	ArraySliceReference.index()	Returns the index expression of the array slice.

Uses of Expression in dev.civl.mc.model.IF.location

Methods in dev.civl.mc.model.IF.location that return Expression

Modifier and Type	Method	Description
Expression	Location.pathCondition()	returns the path condition of this location from the start location

Methods in dev.civl.mc.model.IF.location with parameters of type Expression

Modifier and Type	Method	Description
void	Location.setPathcondition(Expression expression)

Uses of Expression in dev.civl.mc.model.IF.statement

Methods in dev.civl.mc.model.IF.statement that return Expression

Modifier and Type	Method	Description
Expression[]	UpdateStatement.arguments()
Expression	UpdateStatement.collator()
Expression	CivlParForSpawnStatement.domain()	returns the domain according to which processes will be spawned.
Expression	DomainIteratorStatement.domain()	Returns the iteration domain expression, which is the expression following the colon.
Expression	NoopStatement.expression()
Expression	ReturnStatement.expression()
Expression	CallOrSpawnStatement.functionExpression()
Expression	MallocStatement.getScopeExpression()	The first argument to the $malloc function is an expression of type pointer-to-heap.
Expression	MallocStatement.getSizeExpression()	The second argument to the $malloc function is an integer expression specifying the size (number of bytes) to malloc.
Expression	Statement.guard()
Expression	AssignStatement.rhs()

Methods in dev.civl.mc.model.IF.statement that return types with arguments of type Expression

Modifier and Type	Method	Description
List<Expression>	CallOrSpawnStatement.arguments()
List<Pair<LHSExpression,Expression>>	ParallelAssignStatement.assignments()

Methods in dev.civl.mc.model.IF.statement with parameters of type Expression

Modifier and Type	Method	Description
CallOrSpawnStatement	CallOrSpawnStatement.replaceWith(ConditionalExpression oldExpression, Expression newExpression)
Statement	Statement.replaceWith(ConditionalExpression oldExpression, Expression newExpression)	Return a new statement by copying this statement and modifying it as well as its guard by replacing a certain conditional expression with a expression, used when translating away conditional expression WITHOUT introducing temporary variables.
void	ReturnStatement.setExpression(Expression expression)
void	Statement.setGuard(Expression guard)

Method parameters in dev.civl.mc.model.IF.statement with type arguments of type Expression

Modifier and Type	Method	Description
void	CallOrSpawnStatement.setArguments(List<Expression> arguments)

Uses of Expression in dev.civl.mc.model.IF.type

Methods in dev.civl.mc.model.IF.type that return Expression

Modifier and Type	Method	Description
Expression	CIVLCompleteArrayType.extent()

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

Methods in dev.civl.mc.semantics.IF with parameters of type Expression

Modifier and Type	Method	Description
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)
Triple<State,CIVLFunction,Integer>	Evaluator.evaluateFunctionIdentifier(State state, int pid, Expression functionPointer, CIVLSource source)	Evaluates a function pointer expression.
Evaluation	LibraryEvaluator.evaluateGuard(CIVLSource source, State state, int pid, String function, Expression[] arguments)	Evaluates the guard of a system function.
MemoryUnitSet	MemoryUnitExpressionEvaluator.evaluateMemoryUnit(State state, Pair<Scope,dev.civl.sarl.IF.expr.SymbolicExpression[]> parameterScope, int pid, Expression muExpr)	Evaluates the memory unit represented by an expression in a contract.
Evaluation	Executor.execute_printf(CIVLSource source, State state, int pid, String process, Expression[] arguments, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues, boolean forcePrint)
Pair<State,String>	SymbolicAnalyzer.expressionEvaluation(State state, int pid, Expression expression, boolean resultOnly)	Compute a friendly string representation of an expression's evaluation.
Triple<State,StringBuffer,Boolean>	Evaluator.getString(CIVLSource source, State state, int pid, String process, Expression charPointerExpr, dev.civl.sarl.IF.expr.SymbolicExpression charPointer)	extracts a string based on a given character pointer or string literal.
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.