Uses of Class
dev.civl.mc.util.IF.Pair

Packages that use Pair

Package	Description
dev.civl.mc.dynamic.IF	Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
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.expression	Submodule model.expression defines expression in CIVL.
dev.civl.mc.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
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 Pair in dev.civl.mc.dynamic.IF

Methods in dev.civl.mc.dynamic.IF that return Pair

Modifier and Type	Method	Description
Pair<dev.civl.sarl.IF.expr.NumericExpression,dev.civl.sarl.IF.expr.NumericExpression>	SymbolicUtility.arithmeticIntDivide(dev.civl.sarl.IF.expr.NumericExpression dividend, dev.civl.sarl.IF.expr.NumericExpression denominator)	This function does an arithmetic integer division, returns the quotient and remainder

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

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

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.

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

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

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 Pair

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

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

Modifier and Type	Method	Description
ArrayLambdaExpression	ModelFactory.arrayLambdaExpression(CIVLSource source, CIVLArrayType arrayType, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new array lambda expression.
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.
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.

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

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

Modifier and Type	Method	Description
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<Pair<Variable,IntegerLiteralExpression>>	DerivativeCallExpression.partials()

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

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

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

Uses of Pair in dev.civl.mc.predicate.IF

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

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 Pair

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 Pair in dev.civl.mc.semantics.IF

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

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.
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.
Pair<State,String>	SymbolicAnalyzer.expressionEvaluation(State state, int pid, Expression expression, boolean resultOnly)	Compute a friendly string representation of an expression's evaluation.
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.

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

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

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

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

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