Uses of Interface
dev.civl.mc.state.IF.State

Packages that use State

Package	Description
dev.civl.mc.analysis.IF	Module analysis provides a list of analyzers for static/runtime analyzing of a program.
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.predicate.IF	Module predicate defines predicates that are required to hold for any CIVL-C programs.
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 State in dev.civl.mc.analysis.IF

Methods in dev.civl.mc.analysis.IF with parameters of type State

Modifier and Type	Method	Description
void	CodeAnalyzer.analyze(State state, int pid, CallOrSpawnStatement statement, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues)	Analyzes a call statement.
static void	Analysis.analyzeCall(List<CodeAnalyzer> analyzers, State state, int pid, CallOrSpawnStatement statement, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Analyzes a call statement at a certain state.

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

Methods in dev.civl.mc.kripke.IF that return State

Modifier and Type	Method	Description
State	TraceStep.getFinalState()
State	AtomicStep.getPostState()	Returns the resulting state of this atomic step.

Methods in dev.civl.mc.kripke.IF that return types with arguments of type State

Modifier and Type	Method	Description
abstract Map<dev.civl.sarl.IF.expr.BooleanExpression,Set<Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression[]>>>	CIVLStateManager.collectedOutputs()	Outputs collected for the model during the search.
static dev.civl.gmc.dpor.DependencyAnalyzer<State,Transition>	Kripkes.newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State,Transition> manager, StateFactory stateFactory, dev.civl.mc.kripke.common.SimpleEnabler enabler)

Methods in dev.civl.mc.kripke.IF with parameters of type State

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.
dev.civl.sarl.IF.expr.BooleanExpression	Enabler.getGuard(Statement statement, int pid, State state)	Computes the guard of a statement.
void	TraceStep.setFinalState(State finalState)	Set final state to the trace step.
void	AtomicStep.setPostState(State state)	Updates the resulting state of this atomic step.

Method parameters in dev.civl.mc.kripke.IF with type arguments of type State

Modifier and Type	Method	Description
static dev.civl.gmc.dpor.DependencyAnalyzer<State,Transition>	Kripkes.newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State,Transition> manager, StateFactory stateFactory, dev.civl.mc.kripke.common.SimpleEnabler enabler)

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

Methods in dev.civl.mc.log.IF that return State

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.
State	CIVLExecutionException.state()

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

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 State

Modifier	Constructor	Description
	CIVLExecutionException(CIVLProperty property, CIVLException.Certainty certainty, String message, State state)	Constructs new CIVLExecutionException with no associated process.
	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 State in dev.civl.mc.predicate.IF

Methods in dev.civl.mc.predicate.IF that return types with arguments of type State

Modifier and Type	Method	Description
Map<dev.civl.sarl.IF.expr.BooleanExpression,Set<Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression[]>>>	FunctionalEquivalence.specificationOutputs()	The specification output of this predicate, which is a list of tuples of path condition and a map of (output) variables and their values.

Method parameters in dev.civl.mc.predicate.IF with type arguments of type State

Modifier and Type	Method	Description
static FunctionalEquivalence	Predicates.newFunctionalEquivalence(dev.civl.sarl.IF.SymbolicUniverse universe, SymbolicAnalyzer symbolicAnalyzer, String[] outputNames, Map<dev.civl.sarl.IF.expr.BooleanExpression,Set<Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression[]>>> specOutputs)

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

Fields in dev.civl.mc.semantics.IF declared as State

Modifier and Type	Field	Description
State	Evaluation.state	The (possibly) new state resulting from side-effects arising from a certain evaluation.
State	TypeEvaluation.state

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

Modifier and Type	Method	Description
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.
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.

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

Modifier and Type	Method	Description
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.
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.

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

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.
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.
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.
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.
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.
StringBuffer	SymbolicAnalyzer.inputVariablesToStringBuffer(State state)
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.
Pair<dev.civl.sarl.IF.expr.BooleanExpression,dev.civl.sarl.IF.ValidityResult.ResultType>	SymbolicAnalyzer.isDerefablePointer(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Is this a derefable pointer? In other words, check if the pointer can be dereferenced safely.
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.memoryUnitToString(State state, MemoryUnit mu)	Pretty representation of a memory unit.
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)
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.stateInformation(State state)	Computes the user-friendly and brief string representation of a state.
StringBuffer	SymbolicAnalyzer.statementEvaluation(State preState, State postState, int pid, Statement statement)
StringBuffer	SymbolicAnalyzer.stateToString(State state)	Computes the user-friendly and complete string representation of a state.
StringBuffer	SymbolicAnalyzer.stateToString(State state, int lastSavedState, int sequenceId)	Computes the user-friendly and complete string representation of a state.
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.

Constructors in dev.civl.mc.semantics.IF with parameters of type State

Modifier	Constructor	Description
	Evaluation(State state, dev.civl.sarl.IF.expr.SymbolicExpression value)	Creates a new instance of evaluation.
	TypeEvaluation(State state, dev.civl.sarl.IF.type.SymbolicType type)

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

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

Modifier and Type	Field	Description
protected State	CIVLStateException.state

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

Modifier and Type	Method	Description
State	StateFactory.addProcess(State state, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)	Adds a new process.
State	StateFactory.addProcess(State state, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)	Adds a new process.
State	StateFactory.addReadWriteRecords(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression memValue, boolean isRead)	Records a collection of pointers to changed memory locations.
State	StateFactory.addToPathcondition(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression clause)	Add a boolean value clause to the path condition of the given state.
State	StateFactory.canonic(State state, boolean collectProcesses, boolean collectScopes, boolean collectHeaps, boolean collectSymbolicConstants, boolean simplify, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)	Return the "canonical" version of the given state.
State	StateFactory.collectHeaps(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)	Performs a garbage collection and canonicalization of heaps.
State	StateFactory.collectProcesses(State state)	Performs a garbage collection and canonicalization of the process states.
State	StateFactory.collectScopes(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)	Performs a garbage collection and canonicalization of dynamic scopes.
State	StateFactory.deallocate(State state, dev.civl.sarl.IF.expr.SymbolicExpression heapObjectPointer, dev.civl.sarl.IF.expr.SymbolicExpression scopeOfPointer, int mallocId, int index)	Deallocates a heap object from the heap of a given dyscope.
State	StateFactory.emptyState(int nprocs)	Creates an empty state which contains no dyscopes but an array of process states with length 'nprocs'.
State	StateFactory.enterAtomic(State state, int pid)	Process pid enters a new atomic section.
State	StateFactory.getAtomicLock(State state, int pid)	Declares that the process with the given PID now owns the atomic lock.
State	StateFactory.initialState(Model model)	Returns the canonic, initial state for a CIVL Model.
State	StateFactory.leaveAtomic(State state, int pid)	Process pid leaves an atomic section. Precondition: in the given state, the process pid holds the atomic lock and its atomic count is greater than zero. The atomic count is decremented by 1 after this method; if the resultant atomic count is 0, then the atomic lock is released as well.
State	StateFactory.popAssumption(State state, int pid)
State	StateFactory.popCallStack(State state, int pid)	Pops an entry off the call stack for a process.
State	StateFactory.popReadWriteSet(State state, int pid, boolean isRead)
State	StateFactory.pushAssumption(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression assumption)
State	StateFactory.pushCallStack(State state, int pid, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Pushes a new entry onto the call stack for a process.
State	StateFactory.pushCallStack(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Pushes a new entry onto the call stack for a process.
State	StateFactory.pushContract(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Pushes a new frame onto the call stack where static scope of the frame is the contract scope of a function.
State	StateFactory.pushEmptyReadWrite(State state, int pid, boolean isRead)
State	StateFactory.releaseAtomicLock(State state)	Releases the atomic lock, by updating the atomic lock variable with the undefined process value.
State	StateFactory.removeProcess(State state, int pid)	Removes a process from the state.
State	StateFactory.setLocation(State state, int pid, Location location)	Sets the location of a process.
State	StateFactory.setLocation(State state, int pid, Location location, boolean accessChanged)	Sets the location of a process.
State	StateFactory.setProcessState(State state, ProcessState processState)	Updates the state by replacing the process state with the given one where the PID of the old process state is the same as the given process state.
State	StateFactory.setVariable(State state, int vid, int scopeId, dev.civl.sarl.IF.expr.SymbolicExpression value)	Updates the value assigned to a variable in the state.
State	StateFactory.setVariable(State state, Variable variable, int pid, dev.civl.sarl.IF.expr.SymbolicExpression value)	Updates the value assigned to a variable in the state.
State	StateFactory.simplify(State state)	Simplifies all variable values in the state, using the path condition as the simplification context.
State	StateFactory.simplify(State state, int pid)
State	StateFactory.simplify(State state, int pid, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)
State	StateFactory.simplify(State state, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)
State	CIVLHeapException.state()
State	CIVLStateException.state()
State	StateFactory.terminateProcess(State state, int pid)	Sets the process state for the designated process to be the process state with the empty stack.

Methods in dev.civl.mc.state.IF that return types with arguments of type State

Modifier and Type	Method	Description
Pair<State,dev.civl.sarl.IF.expr.SymbolicConstant>	StateFactory.getFreshSymbol(State state, int index, dev.civl.sarl.IF.type.SymbolicType type)	Creates a fresh symbolic constant of the given type at the given state.
Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.malloc(State state, int pid, int dyscopeID, int mallocID, dev.civl.sarl.IF.type.SymbolicType elementType, dev.civl.sarl.IF.expr.NumericExpression elementCount)	Allocates an object for the given malloc ID in the heap of the given dyscope.
Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.malloc(State state, int dyscopeID, int mallocID, dev.civl.sarl.IF.expr.SymbolicExpression heapObject)	Allocates an object, of the given value, for the given malloc ID in the heap of the given dyscope.
Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.valueSetHavoc(State state, dev.civl.sarl.IF.expr.SymbolicExpression value, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)	Performs a value-set havoc operation that replaces parts of a value specified by a value set template with fresh symbolic constants using the havoc prefix (Y).

Methods in dev.civl.mc.state.IF with parameters of type State

Modifier and Type	Method	Description
State	StateFactory.addProcess(State state, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)	Adds a new process.
State	StateFactory.addProcess(State state, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)	Adds a new process.
State	StateFactory.addReadWriteRecords(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression memValue, boolean isRead)	Records a collection of pointers to changed memory locations.
State	StateFactory.addToPathcondition(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression clause)	Add a boolean value clause to the path condition of the given state.
State	StateFactory.canonic(State state, boolean collectProcesses, boolean collectScopes, boolean collectHeaps, boolean collectSymbolicConstants, boolean simplify, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)	Return the "canonical" version of the given state.
State	StateFactory.collectHeaps(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)	Performs a garbage collection and canonicalization of heaps.
State	StateFactory.collectProcesses(State state)	Performs a garbage collection and canonicalization of the process states.
State	StateFactory.collectScopes(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)	Performs a garbage collection and canonicalization of dynamic scopes.
State	StateFactory.deallocate(State state, dev.civl.sarl.IF.expr.SymbolicExpression heapObjectPointer, dev.civl.sarl.IF.expr.SymbolicExpression scopeOfPointer, int mallocId, int index)	Deallocates a heap object from the heap of a given dyscope.
State	StateFactory.enterAtomic(State state, int pid)	Process pid enters a new atomic section.
State	StateFactory.getAtomicLock(State state, int pid)	Declares that the process with the given PID now owns the atomic lock.
Pair<State,dev.civl.sarl.IF.expr.SymbolicConstant>	StateFactory.getFreshSymbol(State state, int index, dev.civl.sarl.IF.type.SymbolicType type)	Creates a fresh symbolic constant of the given type at the given state.
Map<Variable,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.inputVariableValueMap(State state)	Returns the map of input variable and their value at the given state; empty map if there are no input variables.
boolean	StateFactory.isDescendantOf(State state, int ancestor, int descendant)	Checks if one dyscope is strictly the descendant of the other (not equal to).
State	StateFactory.leaveAtomic(State state, int pid)	Process pid leaves an atomic section. Precondition: in the given state, the process pid holds the atomic lock and its atomic count is greater than zero. The atomic count is decremented by 1 after this method; if the resultant atomic count is 0, then the atomic lock is released as well.
boolean	StateFactory.lockedByAtomic(State state)	Checks if any process at the state is holding the atomic lock, i.e, the process is executing some atomic blocks.
int	StateFactory.lowestCommonAncestor(State state, int one, int another)	Computes the lowest common ancestor of two given dyscopes.
Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.malloc(State state, int pid, int dyscopeID, int mallocID, dev.civl.sarl.IF.type.SymbolicType elementType, dev.civl.sarl.IF.expr.NumericExpression elementCount)	Allocates an object for the given malloc ID in the heap of the given dyscope.
Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.malloc(State state, int dyscopeID, int mallocID, dev.civl.sarl.IF.expr.SymbolicExpression heapObject)	Allocates an object, of the given value, for the given malloc ID in the heap of the given dyscope.
DynamicMemoryLocationSet	StateFactory.peekReadWriteSet(State state, int pid, boolean isRead)
State	StateFactory.popAssumption(State state, int pid)
State	StateFactory.popCallStack(State state, int pid)	Pops an entry off the call stack for a process.
State	StateFactory.popReadWriteSet(State state, int pid, boolean isRead)
int	StateFactory.processInAtomic(State state)	Returns the PID of the process that holds the atomic lock at a certain state
State	StateFactory.pushAssumption(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression assumption)
State	StateFactory.pushCallStack(State state, int pid, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Pushes a new entry onto the call stack for a process.
State	StateFactory.pushCallStack(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Pushes a new entry onto the call stack for a process.
State	StateFactory.pushContract(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)	Pushes a new frame onto the call stack where static scope of the frame is the contract scope of a function.
State	StateFactory.pushEmptyReadWrite(State state, int pid, boolean isRead)
State	StateFactory.releaseAtomicLock(State state)	Releases the atomic lock, by updating the atomic lock variable with the undefined process value.
State	StateFactory.removeProcess(State state, int pid)	Removes a process from the state.
State	StateFactory.setLocation(State state, int pid, Location location)	Sets the location of a process.
State	StateFactory.setLocation(State state, int pid, Location location, boolean accessChanged)	Sets the location of a process.
State	StateFactory.setProcessState(State state, ProcessState processState)	Updates the state by replacing the process state with the given one where the PID of the old process state is the same as the given process state.
State	StateFactory.setVariable(State state, int vid, int scopeId, dev.civl.sarl.IF.expr.SymbolicExpression value)	Updates the value assigned to a variable in the state.
State	StateFactory.setVariable(State state, Variable variable, int pid, dev.civl.sarl.IF.expr.SymbolicExpression value)	Updates the value assigned to a variable in the state.
State	StateFactory.simplify(State state)	Simplifies all variable values in the state, using the path condition as the simplification context.
State	StateFactory.simplify(State state, int pid)
State	StateFactory.simplify(State state, int pid, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)
State	StateFactory.simplify(State state, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)
State	StateFactory.terminateProcess(State state, int pid)	Sets the process state for the designated process to be the process state with the empty stack.
Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.valueSetHavoc(State state, dev.civl.sarl.IF.expr.SymbolicExpression value, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)	Performs a value-set havoc operation that replaces parts of a value specified by a value set template with fresh symbolic constants using the havoc prefix (Y).

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

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)