Uses of Interface
dev.civl.mc.model.IF.CIVLSource

Packages that use CIVLSource

Package	Description
dev.civl.mc.dynamic.IF	Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
dev.civl.mc.log.IF	Module log provides the data structure for logging errors during verification.
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.statement	Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.
dev.civl.mc.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.

Uses of CIVLSource in dev.civl.mc.dynamic.IF

Methods in dev.civl.mc.dynamic.IF with parameters of type CIVLSource

Modifier and Type	Method	Description
StringBuffer	SymbolicUtility.charArrayToString(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression charArray, int startIndex, boolean forPrint)	Constructs the string representation of an array of characters, which contains at least one '\0' character, starting from the given index and ending at the index of '\0' minus one.
int	SymbolicUtility.extractInt(CIVLSource source, dev.civl.sarl.IF.expr.NumericExpression expression)	Gets a Java concrete int from a symbolic expression
int	SymbolicUtility.extractIntField(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression tuple, dev.civl.sarl.IF.object.IntObject fieldIndex)	Gets a concrete Java int from the field of a symbolic expression of tuple type or throws exception.
int	SymbolicUtility.getArrayIndex(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a pointer to a certain element of some array, returns the index of the element that the pointer points to.
int	SymbolicUtility.getVariableId(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a pointer value, returns the variable ID component of that value.
boolean	SymbolicUtility.isEmptyDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain, int dim, CIVLSource source)	Returns true if and only if the given domain is empty which means there is no elements in the domain.
boolean	SymbolicUtility.isMallocPointer(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Is the given pointer the result of some malloc/handle create operation?

Uses of CIVLSource in dev.civl.mc.log.IF

Methods in dev.civl.mc.log.IF with parameters of type CIVLSource

Modifier and Type	Method	Description
State	CIVLErrorLogger.logError(CIVLSource source, State state, int pid, StringBuffer stateString, dev.civl.sarl.IF.expr.BooleanExpression claim, dev.civl.sarl.IF.ValidityResult.ResultType resultType, CIVLProperty property, String message)	Report a (possible) error detected in the course of evaluating an expression.
void	CIVLErrorLogger.logSimpleError(CIVLSource source, State state, int pid, String process, StringBuffer stateString, CIVLProperty property, String message)	Checks whether the path condition is satisfiable and logs an error if it is (or might be).

Constructors in dev.civl.mc.log.IF with parameters of type CIVLSource

Modifier	Constructor	Description
	CIVLExecutionException(CIVLProperty property, CIVLException.Certainty certainty, String message, State state, CIVLSource source)	Constructs new CIVLExecutionException with no associated process.
	CIVLExecutionException(CIVLProperty property, CIVLException.Certainty certainty, String process, String message, State state, int pid, CIVLSource source)	Constructs a new CIVLExecutionException with an associated process.
	CIVLExecutionException(CIVLProperty property, CIVLException.Certainty certainty, String process, String message, State state, int pid, CIVLSource source, StringBuffer stateString)	Constructs a new CIVLExecutionException with an associated process and stateString.

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

Fields in dev.civl.mc.model.IF declared as CIVLSource

Modifier and Type	Field	Description
protected CIVLSource	CIVLException.source	Source of the element that led to exception, for error reporting.

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

Modifier and Type	Method	Description
CIVLSource	CIVLException.getSource()
CIVLSource	Sourceable.getSource()
CIVLSource	ModelFactory.sourceOf(dev.civl.abc.ast.node.IF.ASTNode node)	Get the CIVL source of an AST node
CIVLSource	ModelFactory.sourceOf(dev.civl.abc.token.IF.Source abcSource)	Translate ABC source into CIVL source
CIVLSource	ModelFactory.sourceOfBeginning(dev.civl.abc.ast.node.IF.ASTNode node)	Get the CIVL source of the beginning of an AST node
CIVLSource	ModelFactory.sourceOfEnd(dev.civl.abc.ast.node.IF.ASTNode node)	Get the CIVL source of the end of an AST node
CIVLSource	ModelFactory.sourceOfSpan(dev.civl.abc.ast.node.IF.ASTNode node1, dev.civl.abc.ast.node.IF.ASTNode node2)	Get the CIVL span source of two AST nodes
CIVLSource	ModelFactory.sourceOfSpan(dev.civl.abc.token.IF.Source abcSource1, dev.civl.abc.token.IF.Source abcSource2)	Translate the span of two ABC sources into CIVL source
CIVLSource	ModelFactory.sourceOfSpan(CIVLSource source1, CIVLSource source2)	Get the span of two CIVL sources
CIVLSource	ModelFactory.sourceOfToken(dev.civl.abc.token.IF.CivlcToken token)	Get the CIVL source of a C token
CIVLSource	ModelFactory.systemSource()	Returns a source object representing a system-defined object with no link to actual source code.

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

Modifier and Type	Method	Description
AbstractFunction	ModelFactory.abstractFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, int continuity, String attribute)	Generate an abstract function.
AbstractFunctionCallExpression	ModelFactory.abstractFunctionCallExpression(CIVLSource source, AbstractFunction function, List<Expression> arguments)	An expression for a call to an abstract function.
AddressOfExpression	ModelFactory.addressOfExpression(CIVLSource source, LHSExpression operand)	Returns a new address-of expression (invalid input: '&e') with given operand.
ArrayLambdaExpression	ModelFactory.arrayLambdaExpression(CIVLSource source, CIVLArrayType arrayType, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new array lambda expression.
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.
BooleanLiteralExpression	ModelFactory.booleanLiteralExpression(CIVLSource source, boolean value)	A boolean literal expression.
BoundVariableExpression	ModelFactory.boundVariableExpression(CIVLSource source, Identifier name, CIVLType type)	An expression for a bound variable.
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
CharLiteralExpression	ModelFactory.charLiteralExpression(CIVLSource sourceOf, char value)	Creates a character literal expression with the given character value.
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.
CompoundLiteralExpression	ModelFactory.compoundLiteralExpression(CIVLSource source, Scope exprScope, CIVLType type, boolean isStringLiteral)	Creates a new instance of a compound literal expression.
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.
DerivativeCallExpression	ModelFactory.derivativeCallExpression(CIVLSource source, AbstractFunction function, List<Pair<Variable,IntegerLiteralExpression>> partials, List<Expression> arguments)	An expression for a call to the derivative of an abstract function.
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.
VariableExpression	ModelFactory.domSizeVariable(CIVLSource source, Scope scope)
DotExpression	ModelFactory.dotExpression(CIVLSource source, Expression struct, int fieldIndex)	A dot expression is a reference to a struct field.
DynamicTypeOfExpression	ModelFactory.dynamicTypeOfExpression(CIVLSource source, CIVLType type)	Returns a "DynamicTypeOf" expression with the given type argument.
ExtendedQuantifiedExpression	ModelFactory.extendedQuantifiedExpression(CIVLSource source, CIVLType type, dev.civl.abc.ast.node.IF.acsl.ExtendedQuantifiedExpressionNode.ExtendedQuantifier quant, Expression lo, Expression hi, Expression function)
CIVLFunction	ModelFactory.function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation)	Create a new function.
Expression	ModelFactory.functionGuardExpression(CIVLSource source, Expression function, List<Expression> arguments)
FunctionIdentifierExpression	ModelFactory.functionIdentifierExpression(CIVLSource source, CIVLFunction function)	creates a function identifier expression.
Identifier	ModelFactory.getLiteralDomCounterIdentifier(CIVLSource source, int count)	Get the name of the counter variable for the for loop on a literal domain
NoopStatement	ModelFactory.gotoBranchStatement(CIVLSource civlSource, Location source, String label)	A goto branch statement is of the form goto label; .
HereOrRootExpression	ModelFactory.hereOrRootExpression(CIVLSource source, boolean isRoot)
Identifier	ModelFactory.identifier(CIVLSource source, String name)	Get an identifier with the given name.
NoopStatement	ModelFactory.ifElseBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isIf)	An if-else branch statement is introduced to translate if-else statement.
InitialValueExpression	ModelFactory.initialValueExpression(CIVLSource source, Variable variable)	Returns an "initial value" expression for the given variable.
IntegerLiteralExpression	ModelFactory.integerLiteralExpression(CIVLSource source, BigInteger value)	An integer literal expression.
LambdaExpression	ModelFactory.lambdaExpression(CIVLSource source, CIVLFunctionType functionType, Variable variable, Expression expression)	Creates a new lambda expression.
Location	ModelFactory.location(CIVLSource source, Scope scope)	Create a new location.
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.
LoopContract	ModelFactory.loopContract(CIVLSource civlSource, Location loopLocation, List<Expression> loopInvariants, List<LHSExpression> loopAssigns, List<Expression> loopVariants)	Creates a LoopContract instance
MallocStatement	ModelFactory.mallocStatement(CIVLSource civlSource, Location source, LHSExpression lhs, CIVLType staticElementType, Expression scopeExpression, Expression sizeExpression, int mallocId, Expression guard)	Create a new malloc statement
MemoryUnitExpression	ModelFactory.memoryUnitExpression(CIVLSource source, Variable variable, CIVLType objetType, MemoryUnitReference reference, boolean writable, boolean hasPinterRef)	creates a memory unit expression.
Model	ModelFactory.model(CIVLSource source, CIVLFunction system, dev.civl.abc.program.IF.Program program)	Create a new model.
Variable	ModelFactory.newAnonymousVariable(CIVLSource sourceOf, Scope scope, CIVLType type)	Create a variable of the given type and add it to the given scope.
Variable	ModelFactory.newAnonymousVariableForArrayLiteral(CIVLSource sourceOf, Scope scope, CIVLArrayType type)	Creates an anonymous variable of array type in a certain scope.
Variable	ModelFactory.newAnonymousVariableForConstantArrayLiteral(CIVLSource sourceOf, CIVLArrayType type, dev.civl.sarl.IF.expr.SymbolicExpression value)	Creates an anonymous variable of array type in the static constant scope.
CIVLFunction	ModelFactory.nondetFunction(CIVLSource source, Identifier name, CIVLType returnType, Scope containingScope)
NoopStatement	ModelFactory.noopStatement(CIVLSource civlSource, Location source, Expression expression)	A noop statement with the default guard of true.
NoopStatement	ModelFactory.noopStatementForVariableDeclaration(CIVLSource civlSource, Location source)	A temporary noop statement with the true guard
NoopStatement	ModelFactory.noopStatementTemporary(CIVLSource civlSource, Location source)	A temporary noop statement with the true guard
NoopStatement	ModelFactory.noopStatementWtGuard(CIVLSource civlSource, Location source, Expression guard)	A noop statement with an explicit guard expression.
Nothing	ModelFactory.nothing(CIVLSource source)
Expression	ModelFactory.nullPointerExpression(CIVLPointerType pointerType, CIVLSource source)	Generate a null pointer expression
ParallelAssignStatement	ModelFactory.parallelAssignStatement(CIVLSource source, List<Pair<LHSExpression,Expression>> assignPairs)
VariableExpression	ModelFactory.parProcsVariable(CIVLSource source, CIVLType type, Scope scope)
ProcnullExpression	ModelFactory.procnullExpression(CIVLSource source)	Creates a $proc_null constant expression.
QuantifiedExpression	ModelFactory.quantifiedExpression(CIVLSource source, QuantifiedExpression.Quantifier quantifier, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new quantified expression.
RealLiteralExpression	ModelFactory.realLiteralExpression(CIVLSource source, BigDecimal value)	A real literal 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).
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.
Scope	ModelFactory.scope(CIVLSource source, Scope parent, List<Variable> variables, CIVLFunction function)	Create a new scope.
ScopeofExpression	ModelFactory.scopeofExpression(CIVLSource source, LHSExpression argument)	Creates a new $scopeof expression using the given argument.
SelfExpression	ModelFactory.selfExpression(CIVLSource source)	A self expression.
void	Sourceable.setCIVLSource(CIVLSource source)
SizeofExpression	ModelFactory.sizeofExpressionExpression(CIVLSource source, Expression argument)	Returns a new expression of the form "sizeof(e)" where is an expression.
SizeofTypeExpression	ModelFactory.sizeofTypeExpression(CIVLSource source, CIVLType type)	Returns a new "sizeof(t)" expression.
CIVLSource	ModelFactory.sourceOfSpan(CIVLSource source1, CIVLSource source2)	Get the span of two CIVL sources
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.
SystemFunction	ModelFactory.systemFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, String libraryName)	Generate the system function
Expression	ModelFactory.trueExpression(CIVLSource source)	creates a new boolean expression which has the value $true
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.
Variable	ModelFactory.variable(CIVLSource source, CIVLType type, Identifier name, int vid)	Create a new variable.
Variable	ModelFactory.variableAsParameter(CIVLSource source, CIVLType type, Identifier name, int vid)	Create a new variable which is also a parameter of some function.
VariableExpression	ModelFactory.variableExpression(CIVLSource source, Variable variable)	A variable expression.
WildcardExpression	ModelFactory.wildcardExpression(CIVLSource source, CIVLType type)	Creates a wildcard expression ..., which is only used in contract.

Constructors in dev.civl.mc.model.IF with parameters of type CIVLSource

Modifier	Constructor	Description
	CIVLException(String message, CIVLSource source)
	CIVLInternalException(String s, CIVLSource source)
	CIVLSyntaxException(String message, CIVLSource source)
	CIVLUnimplementedFeatureException(String feature, CIVLSource source)

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

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

Modifier and Type	Method	Description
DependsEvent	ContractFactory.newAnyactEvent(CIVLSource source)	Creates a new instance of \anyact event
CallEvent	ContractFactory.newCallEvent(CIVLSource source, CIVLFunction function, List<Expression> arguments)	Creates a new instance of call event.
CompositeEvent	ContractFactory.newCompositeEvent(CIVLSource source, CompositeEvent.CompositeEventOperator op, DependsEvent left, DependsEvent right)	Creates a new instance of composite event.
FunctionBehavior	ContractFactory.newFunctionBehavior(CIVLSource source)	Creates a new function behavior.
FunctionContract	ContractFactory.newFunctionContract(CIVLSource source, Scope scope)	Creates a new function contract.
MemoryEvent	ContractFactory.newMemoryEvent(CIVLSource source, DependsEvent.DependsEventKind kind, Set<Expression> memoryUnits)	Creates a new instance of memory event of the given kind.
NamedFunctionBehavior	ContractFactory.newNamedFunctionBehavior(CIVLSource source, String name)	Creates a new named function behavior
DependsEvent	ContractFactory.newNoactEvent(CIVLSource source)	Creates a new instance of \noact event

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

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

Modifier and Type	Method	Description
void	Statement.setCIVLSource(CIVLSource source)

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

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

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.
State	Executor.assign(CIVLSource source, State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression value)	Assigns a value to the referenced cell in the state.
State	Executor.assign2(CIVLSource source, State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression pointerToVarOrHeapObject, dev.civl.sarl.IF.expr.SymbolicExpression newValueOfVarOrHeapObject, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)	Given a "pointer" to a variable (Variable) or a memory heap object (see SymbolicUtility.isPointerToHeap(SymbolicExpression)), a symbolic expression "newValue" that represents the new value of the variable or the memory heap object and a symbolic expression "valueSetTemplate" of CoreUniverse.valueSetTemplateType(), which refers to a set of regions in the variable or the heap object, this method carves the part that is referred by the "valueSetTemplate" out of the "newValue" and assigns it to the counterpart in the variable or the heap object.
CIVLType	SymbolicAnalyzer.civlTypeOfObjByPointer(CIVLSource soruce, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Computes the CIVL type of the object referring to by the given pointer.
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.
dev.civl.sarl.IF.type.SymbolicType	SymbolicAnalyzer.dynamicTypeOfObjByPointer(CIVLSource source, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Computes the SymbolicType of the object referring to by the given pointer.
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.
Evaluation	Evaluator.evaluateSizeofType(CIVLSource source, State state, int pid, CIVLType type)	Evaluate the size of a CIVL type.
Evaluation	Executor.execute_printf(CIVLSource source, State state, int pid, String process, Expression[] arguments, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues, boolean forcePrint)
CIVLType	SymbolicAnalyzer.getArrayBaseType(State state, CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression arrayPtr)	pre-condition: "arrayPtr" must point to an array "source" is the @{link CIVLSource} of the pointer expression post-condition: the returned CIVLType must not be an array type the returned object cannot be null Get the type of the non-array element of an array by given a pointer to an array
TypeEvaluation	Evaluator.getDynamicType(State state, int pid, CIVLType type, CIVLSource source, boolean isDefinition)	Evaluates the dynamic type of a given CIVL type at a certain state.
dev.civl.sarl.IF.expr.ReferenceExpression	SymbolicAnalyzer.getLeafNodeReference(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer, CIVLSource source)	Spec: Returns a ReferenceExpression object which directly refer to the object which has the physical base type of the pointed array (or object) residing in memory.
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	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.
dev.civl.sarl.IF.expr.SymbolicExpression	SymbolicAnalyzer.getSubArray(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression array, dev.civl.sarl.IF.expr.NumericExpression startIndex, dev.civl.sarl.IF.expr.NumericExpression endIndex, CIVLSource source)	Given an array, a start index, and end index, returns the array which is the subsequence of the given array consisting of the elements in positions start index through end index minus one.
Pair<dev.civl.sarl.IF.expr.BooleanExpression,dev.civl.sarl.IF.ValidityResult.ResultType>	SymbolicAnalyzer.isDefinedPointer(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer, CIVLSource civlSource)	Is this an defined pointer? A pointer is defined if one of the following holds: it can be dereferenced (derefable pointer), e.g., invalid input: '&a', invalid input: '&b'[0] where a is a scalar variable and b is an array of length 5. it is the NULL pointer. it points to the end of an array, e.g., invalid input: '&b'[5] where b is an array of length 5. For the latter two cases, the pointer is called underefable pointer.
List<dev.civl.sarl.IF.expr.ReferenceExpression>	Evaluator.leafNodeReferencesOfType(CIVLSource source, State state, int pid, CIVLType type)
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.
StringBuffer	SymbolicAnalyzer.pathconditionToString(CIVLSource source, State state, String prefix, dev.civl.sarl.IF.expr.BooleanExpression pc)	Pretty representation of a path condition, which is broken into lines if it is in CNF.
dev.civl.sarl.IF.expr.SymbolicExpression	SymbolicAnalyzer.pointerArithmetics(CIVLSource source, State state, boolean isSubtract, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression offset)
void	Executor.printf(PrintStream printStream, CIVLSource source, String process, List<Format> formats, List<StringBuffer> arguments)	If there are insufficient arguments for the format, the behavior is undefined.
List<Format>	Executor.splitFormat(CIVLSource source, StringBuffer formatBuffer)
String	SymbolicAnalyzer.symbolicExpressionToString(CIVLSource source, State state, CIVLType type, dev.civl.sarl.IF.expr.SymbolicExpression symbolicExpression)	Computes the user-friendly string representation of a symbolic expression.

Uses of CIVLSource in dev.civl.mc.state.IF

Fields in dev.civl.mc.state.IF declared as CIVLSource

Modifier and Type	Field	Description
protected CIVLSource	CIVLStateException.source

Methods in dev.civl.mc.state.IF that return CIVLSource

Modifier and Type	Method	Description
CIVLSource	CIVLHeapException.source()
CIVLSource	CIVLStateException.source()

Constructors in dev.civl.mc.state.IF with parameters of type CIVLSource

Modifier	Constructor	Description
	CIVLHeapException(CIVLProperty property, CIVLException.Certainty certainty, State state, String dyscopeName, int dyscopeID, dev.civl.sarl.IF.expr.SymbolicExpression heapValue, int fieldID, int objectID, CIVLHeapException.HeapErrorKind heapError, CIVLSource source)
	CIVLHeapException(CIVLProperty property, CIVLException.Certainty certainty, State state, String dyscopeName, int dyscopeID, dev.civl.sarl.IF.expr.SymbolicExpression heapValue, CIVLHeapException.HeapErrorKind heapError, CIVLSource source)
	CIVLStateException(CIVLProperty property, CIVLException.Certainty certainty, String message, State state, CIVLSource source)