Uses of Class
dev.civl.mc.state.IF.UnsatisfiablePathConditionException

Packages that use UnsatisfiablePathConditionException

Package	Description
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
dev.civl.mc.log.IF	Module log provides the data structure for logging errors during verification.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.

Uses of UnsatisfiablePathConditionException in dev.civl.mc.kripke.IF

Methods in dev.civl.mc.kripke.IF that throw UnsatisfiablePathConditionException

Modifier and Type	Method	Description
BitSet	LibraryEnabler.ampleSet(State state, int pid, CallOrSpawnStatement statement, MemoryUnitSet[] setsReachableRead, MemoryUnitSet[] setsReachableWrite)	Computes the ample set process IDs from a system function call at a given state for a given process.
List<Transition>	LibraryEnabler.enabledTransitions(State state, CallOrSpawnStatement call, dev.civl.sarl.IF.expr.BooleanExpression pathCondition, int pid)	Computes the enabled transitions of a given function call.

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

Methods in dev.civl.mc.log.IF that throw UnsatisfiablePathConditionException

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).

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

Methods in dev.civl.mc.semantics.IF that throw UnsatisfiablePathConditionException

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.assign(State state, int pid, String process, LHSExpression lhs, dev.civl.sarl.IF.expr.SymbolicExpression value, boolean isInitializer)	Assigns a value to the memory location specified by the given left-hand-side expression.
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.
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)
Pair<State,dev.civl.sarl.IF.type.SymbolicArrayType>	Evaluator.evaluateCIVLArrayType(State state, int pid, CIVLArrayType type)	Evaluating the symbolic array type from a CIVLArrayType based on current state and specific process.
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	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.
MemoryUnitSet	MemoryUnitExpressionEvaluator.evaluates(State state, int pid, MemoryUnitExpression memUnit, MemoryUnitSet muSet)	evaluates the static impact memory unit expression which is the result of static analysis
Evaluation	Evaluator.evaluateSizeofType(CIVLSource source, State state, int pid, CIVLType type)	Evaluate the size of a CIVL type.
State	Executor.execute(State state, int pid, Transition transition)	Returns the state that results from executing the statement, or null if path condition becomes unsatisfiable.
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)
Pair<State,String>	SymbolicAnalyzer.expressionEvaluation(State state, int pid, Expression expression, boolean resultOnly)	Compute a friendly string representation of an expression's evaluation.
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.
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.
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.
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.
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.
StringBuffer	SymbolicAnalyzer.statementEvaluation(State preState, State postState, int pid, Statement statement)