Index (CIVL 2.0 main 49 [302247f])

A B C D E F G H I K L M N O P Q R S T U V W Y
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

A

ABS - Static variable in class dev.civl.mc.analysis.IF.Analysis

Name of the absolute value function.

ABSOLUTE - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.DeadlockKind

ABSTRACT_FUNCTION_CALL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

A call to an abstract (mathematical) expression; instance of AbstractFunctionCallExpression.

abstractFunction(CIVLSource, Identifier, Scope, List<Variable>, CIVLType, Scope, int, String) - Method in interface dev.civl.mc.model.IF.ModelFactory

Generate an abstract function.

AbstractFunction - Interface in dev.civl.mc.model.IF

An abstract function is an uninterpreted mathematical function.

AbstractFunction.SpecialRelationKind - Enum Class in dev.civl.mc.model.IF

The kind of a special relation represented by this abstract function

abstractFunctionCallExpression(CIVLSource, AbstractFunction, List<Expression>) - Method in interface dev.civl.mc.model.IF.ModelFactory

An expression for a call to an abstract function.

AbstractFunctionCallExpression - Interface in dev.civl.mc.model.IF.expression

An expression representing a call of an abstract function.

AccuracyAssumptionBuilder - Interface in dev.civl.mc.model.IF

An accuracy assumption builder provides logic for determining additional assumptions that should be added after an assumption involving an abstract function call.

accuracyAssumptions(Expression, Scope) - Method in interface dev.civl.mc.model.IF.AccuracyAssumptionBuilder

Analyze an assumption.

add(int...) - Method in class dev.civl.mc.util.IF.SeqSet

Adds the set represented by the given sequence to this set.

add(MemoryUnit) - Method in interface dev.civl.mc.state.IF.MemoryUnitSet

add(MemoryUnitSet, MemoryUnit) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory

Adds a memory unit to a memory unit set.

add(MemoryUnitSet, SymbolicExpression, StateFactory) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory

addAll(SeqSet) - Method in class dev.civl.mc.util.IF.SeqSet

Adds everything in the given set to this set.

addAnonStatement(Statement) - Method in interface dev.civl.mc.model.IF.ModelFactory

Add the given statement to the anonymous fragment.

addAssignsMemoryUnit(Expression) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Add an assigns clause to this behavior.

addAtomicStep(AtomicStep) - Method in interface dev.civl.mc.kripke.IF.TraceStep

Adds an atomic step to the trace step.

addChild(Scope) - Method in interface dev.civl.mc.model.IF.Scope

addClause(CIVLStatePredicate) - Method in interface dev.civl.mc.predicate.IF.AndPredicate

Add a predicate as one clause of this And predicate.

addDependsEvent(DependsEvent) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Add a depends event to this behavior.

addFinalStatement(Statement) - Method in interface dev.civl.mc.model.IF.Fragment

Add a statement to the final statement set

addFinalStatementSet(Set<Statement>) - Method in interface dev.civl.mc.model.IF.Fragment

Add a set of statements to the final statement set

addFunction(CIVLFunction) - Method in interface dev.civl.mc.model.IF.Model

addFunction(CIVLFunction) - Method in interface dev.civl.mc.model.IF.Scope

addGuardToStartLocation(Expression, ModelFactory) - Method in interface dev.civl.mc.model.IF.Fragment

Add a specified guard to the all statements of the start location.

addHeapFieldObjectType(CIVLType, int) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory

Add the given type as the object type of one of the heap field.

addIncoming(Statement) - Method in interface dev.civl.mc.model.IF.location.Location

addInputVariable(Variable) - Method in interface dev.civl.mc.model.IF.ModelFactory

additionalLibraries - Static variable in class dev.civl.mc.transform.IF.ContractTransformer

additionalLibraries - Static variable in class dev.civl.mc.transform.IF.LoopContractTransformer

addLocation(Location) - Method in interface dev.civl.mc.model.IF.CIVLFunction

addNamedBehavior(NamedFunctionBehavior) - Method in interface dev.civl.mc.model.IF.contract.FunctionContract

Adds a named behavior to the function.

addNewStatement(Statement) - Method in interface dev.civl.mc.model.IF.Fragment

Add a new statement to the fragment, which will be considered the subsequent statement of the current final statements.s

addOutgoing(Statement) - Method in interface dev.civl.mc.model.IF.location.Location

addPossibleValidConsequence(Pair<Expression, Integer>) - Method in interface dev.civl.mc.model.IF.CIVLFunction

Possible valid consequence is a valid contract expression which is POSSIBLE a consequence of the whole contract Notice that consequences only come from requirements

addPostcondition(Expression) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Returns the post condition of this behavior.

addPrecondition(Expression) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Returns the precondition of this behavior.

addProcess(State, CIVLFunction, int, SymbolicExpression[], int, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory

Adds a new process.

addProcess(State, CIVLFunction, SymbolicExpression[], int, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory

Adds a new process.

addReadsMemoryUnit(Expression) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Add a reads clause to this behavior.

addReadWriteRecords(State, int, SymbolicExpression, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory

Records a collection of pointers to changed memory locations.

addReference(DynamicMemoryLocationSet, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.DynamicMemoryLocationSetFactory

Add references in a "memValue" into the given "writeSet", returns a new write set

addReservedName(String) - Static method in class dev.civl.mc.model.IF.ModelConfiguration

add new name to the reserved name set

ADDRESS_OF - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

A C address-of expression invalid input: '&expr', instance of AddressOfExpression.

addressOfExpression(CIVLSource, LHSExpression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Returns a new address-of expression (invalid input: '&e') with given operand.

AddressOfExpression - Interface in dev.civl.mc.model.IF.expression

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.

addSizeofSymbol(SymbolicConstant) - Static method in class dev.civl.mc.model.IF.ModelConfiguration

addStatement(Statement) - Method in interface dev.civl.mc.model.IF.CIVLFunction

addSystemType(String, CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory

Added a type in map of system type, which is the map of types of system libraries, e.g., $gcomm/$comm for comm, $file for stdio, $gbarrier/$barrier for concurrency, etc.

addToPathcondition(State, int, BooleanExpression) - Method in interface dev.civl.mc.state.IF.StateFactory

Add a boolean value clause to the path condition of the given state.

addVariable(Variable) - Method in interface dev.civl.mc.model.IF.Scope

A new variable in this scope.

allComplete(SymbolicArrayType) - Method in interface dev.civl.mc.semantics.IF.ArrayReshaper

allOutgoingPurelyLocal() - Method in interface dev.civl.mc.model.IF.location.Location

This is different from isPurelyLocal(), because the latter is more restricted.

ampleSet(State, int, CallOrSpawnStatement, MemoryUnitSet[], MemoryUnitSet[]) - Method in interface dev.civl.mc.kripke.IF.LibraryEnabler

Computes the ample set process IDs from a system function call at a given state for a given process.

Analysis - Class in dev.civl.mc.analysis.IF

Entry point of the module civl.analysis.

Analysis() - Constructor for class dev.civl.mc.analysis.IF.Analysis

analyze() - Method in interface dev.civl.mc.model.IF.type.CIVLType

This method should be called after all the types are complete; it analyzes the completed type and caches certain information about them in the instance fields.

analyze(State, int, CallOrSpawnStatement, SymbolicExpression[]) - Method in interface dev.civl.mc.analysis.IF.CodeAnalyzer

Analyzes a call statement.

ANALYZE_ABS - Static variable in class dev.civl.mc.config.IF.CIVLConstants

analyzeAbs() - Method in class dev.civl.mc.config.IF.CIVLConfiguration

analyzeAbsO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Analyze abs calls? false by default.

analyzeCall(List<CodeAnalyzer>, State, int, CallOrSpawnStatement, SymbolicExpression[]) - Static method in class dev.civl.mc.analysis.IF.Analysis

Analyzes a call statement at a certain state.

AND - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR

AndPredicate - Interface in dev.civl.mc.predicate.IF

This represents a predicate in CNF, containing a number of predicates, called clauses, i.e., p1 & p2 & ...

AnnotationTransformer - Class in dev.civl.mc.transform.IF

AnnotationTransformer(ASTFactory) - Constructor for class dev.civl.mc.transform.IF.AnnotationTransformer

anonFragment() - Method in interface dev.civl.mc.model.IF.ModelFactory

Returns the current fragment of an assignment statement for an anonymous variable initialization.

ANONYMOUS_VARIABLE_PREFIX - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

prefix for anonymous variables

ANSI_BLACK - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_BLUE - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_BOLD - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_CYAN - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_GREEN - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_OVERSTRIKE - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_OVERSTRIKE_OFF - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_PURPLE - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_RED - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_RESET - Static variable in class dev.civl.mc.util.IF.Utils

0 Normal (clear all) 1 bold 2 dim 4 underline 5 blink 7 reverse 8 blank 9 overstrike 22 normal intensity (cancel bold and blank) 24 underline off 25 blink off 27 reverse off 28 blank off 29 overstrike off 30 black 31 red 32 green 33 yellow 34 blue 35 magenta 36 cyan 37 white 40 black background 41 red background 42 green background

ANSI_UNDERLINE - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_UNDERLINE_OFF - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_WHITE - Static variable in class dev.civl.mc.util.IF.Utils

ANSI_YELLOW - Static variable in class dev.civl.mc.util.IF.Utils

ANYACT - Enum constant in enum class dev.civl.mc.model.IF.contract.DependsEvent.DependsEventKind

apply(UnaryOperator<SymbolicExpression>) - Method in interface dev.civl.mc.dynamic.IF.DynamicMemoryLocationSet

Apply an UnaryOperator on the set of memory location references.

applyReverseFunction(String, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Apply the reverse of a given uninterpreted function.

areArrayShapesPhysicallyEquivalent(ArrayToolBox.ArrayShape, ArrayToolBox.ArrayShape) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Test if two array shapes s0 and s1 are physically equivalent.

areDynamicTypesCompatiableForAssign(SymbolicType, SymbolicType) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer

Check if the dynamic types of the left-hand side (lhs) and right-hand side (rhs) expression are compatible for assignment operation.

arePoint2SameMemoryBlock(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Returns true iff the two pointers are pointing to the same memory block.

areSubtypesScalar() - Method in interface dev.civl.mc.model.IF.type.CIVLType

Are all the sub-types of this type scalar?

argument() - Method in interface dev.civl.mc.model.IF.expression.ScopeofExpression

arguments() - Method in interface dev.civl.mc.model.IF.contract.CallEvent

Returns the arguments of the call event.

arguments() - Method in interface dev.civl.mc.model.IF.expression.AbstractFunctionCallExpression

arguments() - Method in interface dev.civl.mc.model.IF.expression.FunctionGuardExpression

Returns the list of arguments of the corresponding function call statement.

arguments() - Method in interface dev.civl.mc.model.IF.expression.SystemGuardExpression

The list of arguments that this function call uses.

arguments() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

arguments() - Method in interface dev.civl.mc.model.IF.statement.UpdateStatement

arithmeticableExpression(Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Translates an expression to be of the type for arithmetic operations i.e.

arithmeticIntDivide(NumericExpression, NumericExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

This function does an arithmetic integer division, returns the quotient and remainder

array - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArraySlice

the array where the slice is carved out

array() - Method in interface dev.civl.mc.model.IF.expression.SubscriptExpression

ARRAY - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind

ARRAY - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind

ARRAY_LAMBDA - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

an array lambda expression, instance of ArrayLambdaExpression

ARRAY_SLICE - Enum constant in enum class dev.civl.mc.model.IF.expression.reference.MemoryUnitReference.MemoryUnitReferenceKind

The whole variable

ArrayCutter - Interface in dev.civl.mc.semantics.IF

This interface provides methods for dealing with array slices, e.g.

arrayDimensionExtents(SymbolicCompleteArrayType) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Pre-condition: For all the descendant types of the array type, if it is an array type, it must be complete.

arrayElementReferenceAdd(State, int, SymbolicExpression, NumericExpression, CIVLSource) - Method in interface dev.civl.mc.semantics.IF.Evaluator

Do a pointer addition operation on the given pointer with the given offset.

arrayFlatten(SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Reshape a multiple dimensional array of type t to a one dimensional array of type t.

arrayFlatten(SymbolicExpression, ArrayToolBox.ArrayShape) - Method in interface dev.civl.mc.semantics.IF.ArrayReshaper

Reshape a multiple dimensional array of type t to a one dimensional array of type t.

arrayIndiceProjecting(NumericExpression[], ArrayToolBox.ArrayShape, ArrayToolBox.ArrayShape) - Method in interface dev.civl.mc.semantics.IF.ArrayReshaper

Projecting indices I of an array a0 to another array a1, i.e.

arrayIndiceProjecting(NumericExpression[], ArrayToolBox.ArrayShape, ArrayToolBox.ArrayShape) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Projecting indices I of an array a0 to another array a1, i.e.

arrayLambdaExpression(CIVLSource, CIVLArrayType, List<Pair<List<Variable>, Expression>>, Expression, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Creates a new array lambda expression.

ArrayLambdaExpression - Interface in dev.civl.mc.model.IF.expression

A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.

arrayReshape(SymbolicExpression, ArrayToolBox.ArrayShape) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Reshape an array a to the given target shape t.

arrayReshape(SymbolicExpression, ArrayToolBox.ArrayShape, ArrayToolBox.ArrayShape) - Method in interface dev.civl.mc.semantics.IF.ArrayReshaper

Reshape an array a to the given target shape t.

ArrayReshaper - Interface in dev.civl.mc.semantics.IF

This class provides methods for reshaping arrays.

arrayRootPtr(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Given a pointer to an element of an array object, returns a pointer to the whole array object.

ArrayShape() - Constructor for class dev.civl.mc.semantics.IF.ArrayToolBox.ArrayShape

arraySize - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArrayShape

arraySlice(SymbolicExpression, ArrayToolBox.ArrayShape, NumericExpression[], int) - Method in interface dev.civl.mc.semantics.IF.ArrayCutter

Same as

invalid reference

#arraySliceRead(SymbolicExpression, NumericExpression[], NumericExpression)

but the "count" is known as having a concrete value.

arraySlice(SymbolicExpression, ArrayToolBox.ArrayShape, NumericExpression[], NumericExpression) - Method in interface dev.civl.mc.semantics.IF.ArrayCutter

Return an array slice value which is an one-dimensional array of elements of type t, where t is the base type of the given array shape ( ArrayToolBox.ArrayShape.baseType).

ArraySlice() - Constructor for class dev.civl.mc.semantics.IF.ArrayToolBox.ArraySlice

arraySliceRead(SymbolicExpression, NumericExpression[], int) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Same as ArrayToolBox.arraySliceRead(SymbolicExpression, NumericExpression[], NumericExpression) but the "count" is known as having a concrete value.

arraySliceRead(SymbolicExpression, NumericExpression[], NumericExpression) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Returns a symbolic expression representing an array slice which is an one-dimensional array of elements of type t that is carved out from the given array a, where t is associated to to the given indices: {i₀, i₁, ...

arraySliceReference(ArraySliceReference.ArraySliceKind, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory

creates a new array slice reference.

ArraySliceReference - Interface in dev.civl.mc.model.IF.expression.reference

This represents the reference to an array, which could be: element wildcard range

ArraySliceReference.ArraySliceKind - Enum Class in dev.civl.mc.model.IF.expression.reference

arraySlicesSizes(NumericExpression[]) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

pre-condition: length(array_extents) > 0

arraySliceWrite(ArrayToolBox.ArraySlice, SymbolicExpression, ArrayToolBox.ArrayShape, NumericExpression[]) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox

Write an ArrayToolBox.ArraySlice s into the targetArray, starting from the given targetStartIndices

arraySliceWrite(SymbolicExpression, ArrayToolBox.ArrayShape, NumericExpression[], NumericExpression, SymbolicExpression, ArrayToolBox.ArrayShape, NumericExpression[]) - Method in interface dev.civl.mc.semantics.IF.ArrayCutter

Writes an array slice s, which is represents by the three given arguments : sliceArray, sliceIndices, count, into the targetArray, starting from the given targetStartIndices

ArrayToolBox - Interface in dev.civl.mc.semantics.IF

This interface provides a collection of methods that manipulating symbolic expressions whose symbolic type has ARRAY kind.

ArrayToolBox.ArrayShape - Class in dev.civl.mc.semantics.IF

The data structure for describing array shapes, including dimensions, extent for each dimension and slice size for each sub-array with lower dimension.

ArrayToolBox.ArraySlice - Class in dev.civl.mc.semantics.IF

the data structure for describing array slices.

ASSERT - Static variable in class dev.civl.mc.config.IF.CIVLConstants

ASSERT_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Library source files

ASSERTION_VIOLATION - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty

assign(CIVLSource, State, int, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Executor

Assigns a value to the referenced cell in the state.

assign(State, int, String, LHSExpression, SymbolicExpression, boolean) - Method in interface dev.civl.mc.semantics.IF.Executor

Assigns a value to the memory location specified by the given left-hand-side expression.

ASSIGN - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind

Assignment, including atomic lock assignments

assign2(CIVLSource, State, int, SymbolicExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Executor

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.

assignments() - Method in interface dev.civl.mc.model.IF.statement.ParallelAssignStatement

assignsMemoryUnits() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Returns the assigns clause of this behavior.

assignsNothing() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Does this function assigns nothing? That is, is there a assigns \nothing; clause in the contract.

assignStatement(CIVLSource, Location, LHSExpression, Expression, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory

An assignment statement.

AssignStatement - Interface in dev.civl.mc.model.IF.statement

An assignment statement.

assumptions() - Method in interface dev.civl.mc.model.IF.contract.NamedFunctionBehavior

Returns the conjunction of all assumptions of this behavior.

AST - Static variable in class dev.civl.mc.config.IF.CIVLConstants

astO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Show the AST of the program? false by default.

ATOMIC_ENTER - Enum constant in enum class dev.civl.mc.model.IF.location.Location.AtomicKind

ATOMIC_EXIT - Enum constant in enum class dev.civl.mc.model.IF.location.Location.AtomicKind

ATOMIC_LOCK_VARIABLE_INDEX - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

The name of the atomic lock variable of the system scope.

atomicCount() - Method in interface dev.civl.mc.state.IF.ProcessState

atomicEnter(Location) - Method in interface dev.civl.mc.model.IF.ModelFactory

Generate an atomic enter statement

atomicExit(Location) - Method in interface dev.civl.mc.model.IF.ModelFactory

Generate an atomic exit statement

atomicFragment(Fragment, Location, Location) - Method in interface dev.civl.mc.model.IF.ModelFactory

Generate an atomic fragment based on a certain fragment, by adding one location at before and after the fragment to denote the boundary of the atomic block

atomicKind() - Method in interface dev.civl.mc.model.IF.location.Location

Result might be: NONE: a normal location ENTER: the start location of an $atomic block LEAVE: the end location of an $atomic block

AtomicLockAssignStatement - Interface in dev.civl.mc.model.IF.statement

atomicLockVariableExpression() - Method in interface dev.civl.mc.model.IF.ModelFactory

This method is used in Enabler when a process resumes from being blocked and wants to get the atomic lock

AtomicStep - Interface in dev.civl.mc.kripke.IF

This represents an atomic execution step, which represents the execution of exactly one transition.

B

bar - Static variable in class dev.civl.mc.config.IF.CIVLConstants: A string printed before and after titles of sections of output to make them stand out among the clutter.
BARRIER_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of __barrier__ type, which is the object type of the handle $barrier.
baseType - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArrayShape
baseType - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArraySlice: the type of the elements
baseType() - Method in interface dev.civl.mc.model.IF.type.CIVLPointerType: Returns the type of element pointed to.
BIG_O - Enum constant in enum class dev.civl.mc.model.IF.expression.UnaryExpression.UNARY_OPERATOR
biggerAndSet(AtomicInteger, int) - Static method in class dev.civl.mc.util.IF.Utils: Atomically set v1 to a bigger value v2 in a non-blocking manner.
BINARY - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind: A C binary operator expression, e.g., a+b, e/(d-5*c), instance of BinaryExpression.
binaryExpression(CIVLSource, BinaryExpression.BINARY_OPERATOR, Expression, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: A binary expression.
BinaryExpression - Interface in dev.civl.mc.model.IF.expression: A binary operation.
BinaryExpression.BINARY_OPERATOR - Enum Class in dev.civl.mc.model.IF.expression: This defines all CIVL binary operators:
AND: invalid input: '&'invalid input: '&' (logical and); LEFT_SHIFT: invalid input: '<' (bitwise left shift); RIGHT_SHIFT: >> (bitwise right shift); BITAND: invalid input: '&' (bitwise and); BITCOMPLEMENT: ~ (bitwise complement); BITOR: | (bitwise or); BITXOR: ^ (bitwise xor); DIVIDE: / (division); EQUAL: == (equal to); IMPLIES: (implication); LESS_THAN: invalid input: '<' (less than); LESS_THAN_EQUAL: invalid input: '<'= (less than or equal to); MINUS: - (subtraction); MODULO: % (modulo); NOT_EQUAL: != (not equal to); OR: || (logical or); PLUS: + (addition); POINTER_ADD: + (pointer addition); POINTER_SUBTRACT: - (pointer subtraction); TIMES: * (multiplication);
BIT_AND - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
BIT_NOT - Enum constant in enum class dev.civl.mc.model.IF.expression.UnaryExpression.UNARY_OPERATOR
BIT_OR - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
BIT_XOR - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
BITCOMPLEMENT - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
BLACK - Enum constant in enum class dev.civl.mc.util.IF.Utils.Color
BLOCKING - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.MPIModelKind
BLUE - Enum constant in enum class dev.civl.mc.util.IF.Utils.Color
boldText(String) - Static method in class dev.civl.mc.util.IF.Utils
BOOL - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind
BOOLEAN - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind
BOOLEAN_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
booleanExpression(Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Convert an expression to be of boolean-type.
booleanLiteralExpression(CIVLSource, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory: A boolean literal expression.
BooleanLiteralExpression - Interface in dev.civl.mc.model.IF.expression: A literal boolean value.
booleanType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get the boolean primitive type.
bottomToTopIterator() - Method in interface dev.civl.mc.state.IF.ProcessState: Returns an iterator over the entries in the call stack from the bottom to the top.
BOUND_VARIABLE - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
boundVariableExpression(CIVLSource, Identifier, CIVLType) - Method in interface dev.civl.mc.model.IF.ModelFactory: An expression for a bound variable.
BoundVariableExpression - Interface in dev.civl.mc.model.IF.expression: A bound variable is a variable used in a quantified expression.
boundVariableList() - Method in interface dev.civl.mc.model.IF.expression.ArrayLambdaExpression: The list of bound variables.
boundVariableList() - Method in interface dev.civl.mc.model.IF.expression.QuantifiedExpression: The list of bound variables.
BranchConstraints - Class in dev.civl.mc.util.IF
BranchConstraints() - Constructor for class dev.civl.mc.util.IF.BranchConstraints
BROKEN_TIME_VARIABLE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The variable to store broken time information for the time library.
brokenTimeVariable() - Method in interface dev.civl.mc.model.IF.ModelFactory
buildFrameCondition(SymbolicType, SymbolicExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.ValueSetUtility: Builds an assertion stating that all the objects in a variable of varType NOT referred by valueSetTemplate preserve their old values.
buildModel(GMCSection, Program, String, boolean, PrintStream) - Method in interface dev.civl.mc.model.IF.ModelBuilder: Builds the model.
buildStateValue(SymbolicUniverse, int, SymbolicExpression) - Method in interface dev.civl.mc.model.IF.type.CIVLStateType: Translate an integer canonical state id into a symbolic expression
BUNDLE - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
BUNDLE - Static variable in class dev.civl.mc.config.IF.CIVLConstants
BUNDLE_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
BUNDLE_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the name of $bundle type
bundleSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the symbolic type of the bundle type.
bundleType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Gets the CIVL bundle type, which is unique for a given CIVL model.
bundleType() - Method in interface dev.civl.mc.model.IF.Model

C

calculateConstantValue(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.expression.Expression: Calculates the constant value of this expression.
calculateConstantValue(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.statement.Statement
calculateDerefs() - Method in interface dev.civl.mc.model.IF.expression.Expression: Calculate the existence of dereferences in this expression
calculateDerefs() - Method in interface dev.civl.mc.model.IF.statement.Statement: Calculate if this statement contains any dereference expression
call() - Method in interface dev.civl.mc.model.IF.statement.UpdateStatement
CALL - Enum constant in enum class dev.civl.mc.model.IF.contract.DependsEvent.DependsEventKind
CALL_OR_SPAWN - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind: Function call or process spawn
CallEvent - Interface in dev.civl.mc.model.IF.contract: This represents a function call event of a depends clause.
callOrSpawnStatement(CIVLSource, Location, boolean, Expression, List<Expression>, Expression, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates a call or spawn statement.
CallOrSpawnStatement - Interface in dev.civl.mc.model.IF.statement: A function call or spawn.
CALLSTACK - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.ErrorStateEquivalence
callStackToString() - Method in interface dev.civl.mc.state.IF.State: Gets the call stack information (function, location, but no dyscope) of each process and return it as a string buffer object.
callStatement() - Method in interface dev.civl.mc.model.IF.expression.FunctionCallExpression
canonic(MemoryUnitSet) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: Return the "canonical" version of the given memory unit set.
canonic(State, boolean, boolean, boolean, boolean, boolean, Set<CIVLHeapException.HeapErrorKind>) - Method in interface dev.civl.mc.state.IF.StateFactory: Return the "canonical" version of the given state.
CAST - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
castExpression(CIVLSource, CIVLType, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Create a cast expression
CastExpression - Interface in dev.civl.mc.model.IF.expression: A cast of an expression to a different type.
certainty - Variable in exception class dev.civl.mc.state.IF.CIVLStateException
certainty() - Method in exception class dev.civl.mc.log.IF.CIVLExecutionException
certainty() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
certainty() - Method in exception class dev.civl.mc.state.IF.CIVLStateException
CHAR - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind
CHAR - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind
CHAR - Enum constant in enum class dev.civl.mc.semantics.IF.Format.ConversionType
CHAR_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
charArrayToString(CIVLSource, SymbolicExpression, int, boolean) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: 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.
charLiteralExpression(CIVLSource, char) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates a character literal expression with the given character value.
CharLiteralExpression - Interface in dev.civl.mc.model.IF.expression
charType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get the char primitive type.
checkDeadlockKind() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
checkExpressionError() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
child() - Method in interface dev.civl.mc.model.IF.expression.reference.MemoryUnitReference: The child of this reference.
children - Variable in class dev.civl.mc.util.IF.SeqSet.Node: The children nodes.
children() - Method in interface dev.civl.mc.model.IF.Scope
childrenIndexes - Variable in class dev.civl.mc.util.IF.SeqSet.Node: The set consisting of the indexes of the children of this node.
CIVL - Class in dev.civl.mc: The main CIVL class, containing the main method, which provides the command line interface for using CIVL.
CIVL() - Constructor for class dev.civl.mc.CIVL
CIVL_CUDA - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_CUDA_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_LIB_INCLUDE_PATH - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Where the CIVL header files (suffix .h and .cvh) are located.
CIVL_LIB_SRC_PATH - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Resource path to the CIVL library implementations files (.cvl).
CIVL_MACRO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_MPI - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_MPI_BLOCKING - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_MPI_BLOCKING_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_MPI_NONBLOCKING - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_MPI_NONBLOCKING_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_OMP - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_OMP_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_OMP2_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_PAR_FOR_ENTER - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind: $contractVerify statement
CIVL_PTHREAD - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_PTHREAD_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVL_STDIO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVLArrayType - Interface in dev.civl.mc.model.IF.type: The type for an array of T.
CIVLBundleType - Interface in dev.civl.mc.model.IF.type
CIVLC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVLC_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CIVLCompleteArrayType - Interface in dev.civl.mc.model.IF.type: The type for an array of T where the extent is specified.
CIVLCompleteDomainType - Interface in dev.civl.mc.model.IF.type
CIVLConfiguration - Class in dev.civl.mc.config.IF: A CIVLConfiguration object encompasses all the parameters used to configure CIVL for the execution of one or more tasks.
CIVLConfiguration() - Constructor for class dev.civl.mc.config.IF.CIVLConfiguration
CIVLConfiguration(GMCSection) - Constructor for class dev.civl.mc.config.IF.CIVLConfiguration: Constructs a new CIVL configuration object from the command line configuration.
CIVLConfiguration(CIVLConfiguration) - Constructor for class dev.civl.mc.config.IF.CIVLConfiguration
CIVLConstants - Class in dev.civl.mc.config.IF: This class manages all constant configurations of the system.
CIVLConstants() - Constructor for class dev.civl.mc.config.IF.CIVLConstants
CIVLConstants.DeadlockKind - Enum Class in dev.civl.mc.config.IF: Kinds of deadlock: absolute, potential or none.
CIVLConstants.ErrorStateEquivalence - Enum Class in dev.civl.mc.config.IF: Error state equivalence semantics for suppressing logging of redundant errors.
CIVLConstants.MPIModelKind - Enum Class in dev.civl.mc.config.IF: The different MPI implementation model that CIVL provides.
CIVLDomainType - Interface in dev.civl.mc.model.IF.type: This is the only one CIVLDomainType associated to the $domain type in program.
CIVLEnumType - Interface in dev.civl.mc.model.IF.type: An enumeration type.
CIVLErrorLogger - Class in dev.civl.mc.log.IF: CIVLErrorLogger logs all errors of the system.
CIVLErrorLogger(File, String, PrintStream, CIVLConfiguration, GMCConfiguration, StateFactory, SymbolicUniverse, boolean) - Constructor for class dev.civl.mc.log.IF.CIVLErrorLogger: creates a new instance of error logger.
CIVLException - Exception Class in dev.civl.mc.model.IF: Root of CIVL exception hierarchy, representing any kind of event where something goes wrong in CIVL.
CIVLException(String, CIVLSource) - Constructor for exception class dev.civl.mc.model.IF.CIVLException
CIVLException.Certainty - Enum Class in dev.civl.mc.model.IF: A certainty level gages how certain we are that this is error is a real error, i.e., not just a spurious error.
CIVLExecutionException - Exception Class in dev.civl.mc.log.IF: This represents an error during the execution of a program.
CIVLExecutionException(CIVLProperty, CIVLException.Certainty, String, State) - Constructor for exception class dev.civl.mc.log.IF.CIVLExecutionException: Constructs new CIVLExecutionException with no associated process.
CIVLExecutionException(CIVLProperty, CIVLException.Certainty, String, State, CIVLSource) - Constructor for exception class dev.civl.mc.log.IF.CIVLExecutionException: Constructs new CIVLExecutionException with no associated process.
CIVLExecutionException(CIVLProperty, CIVLException.Certainty, String, String, State, int, CIVLSource) - Constructor for exception class dev.civl.mc.log.IF.CIVLExecutionException: Constructs a new CIVLExecutionException with an associated process.
CIVLExecutionException(CIVLProperty, CIVLException.Certainty, String, String, State, int, CIVLSource, StringBuffer) - Constructor for exception class dev.civl.mc.log.IF.CIVLExecutionException: Constructs a new CIVLExecutionException with an associated process and stateString.
civlForEnterFragment(CIVLSource, Location, Expression, List<Variable>, Variable) - Method in interface dev.civl.mc.model.IF.ModelFactory: Returns a new fragment containing a CivlForStatement.
CIVLFunction - Interface in dev.civl.mc.model.IF: A CIVL function.
CIVLFunctionType - Interface in dev.civl.mc.model.IF.type
CIVLHeapException - Exception Class in dev.civl.mc.state.IF: Extends an execution exception with a state at which error occurred.
CIVLHeapException(CIVLProperty, CIVLException.Certainty, State, String, int, SymbolicExpression, int, int, CIVLHeapException.HeapErrorKind, CIVLSource) - Constructor for exception class dev.civl.mc.state.IF.CIVLHeapException
CIVLHeapException(CIVLProperty, CIVLException.Certainty, State, String, int, SymbolicExpression, CIVLHeapException.HeapErrorKind, CIVLSource) - Constructor for exception class dev.civl.mc.state.IF.CIVLHeapException
CIVLHeapException.HeapErrorKind - Enum Class in dev.civl.mc.state.IF
CIVLHeapType - Interface in dev.civl.mc.model.IF.type
CIVLInternalException - Exception Class in dev.civl.mc.model.IF: A CIVL internal exception represents an error that is "not supposed to happen." It can be used like an assertion, whenever you feel that something should always be true.
CIVLInternalException(String, Source) - Constructor for exception class dev.civl.mc.model.IF.CIVLInternalException
CIVLInternalException(String, CIVLSource) - Constructor for exception class dev.civl.mc.model.IF.CIVLInternalException
CIVLInternalException(String, Sourceable) - Constructor for exception class dev.civl.mc.model.IF.CIVLInternalException
CIVLLogEntry - Class in dev.civl.mc.log.IF: This represents an entry in the error log of CIVL.
CIVLLogEntry(CIVLConfiguration, GMCConfiguration, CIVLExecutionException, SymbolicUniverse) - Constructor for class dev.civl.mc.log.IF.CIVLLogEntry
CIVLMacroO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Collect heaps? true by default.
civlMemType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the CIVLMemType.
CIVLMemType - Interface in dev.civl.mc.model.IF.type: A CIVLType representing a set of memory locations.
CIVLMemType.MemoryLocationReference - Interface in dev.civl.mc.model.IF.type: Implementations of CIVLMemType.MemoryLocationReference represent references to a subset of a value of a variable/heap object
civlParForEnterStatement(CIVLSource, Location, Expression, VariableExpression, VariableExpression, CIVLFunction) - Method in interface dev.civl.mc.model.IF.ModelFactory: creates a $parfor enter statement to start the execution of the $parfor.
CivlParForSpawnStatement - Interface in dev.civl.mc.model.IF.statement: This represents the first part of a $parfor construct, i.e., spawning processes according the specified domain.
CIVLPointerType - Interface in dev.civl.mc.model.IF.type: Type of a pointer.
CIVLPrimitiveType - Interface in dev.civl.mc.model.IF.type: A primitive type is a type of which there is only one instance.
CIVLPrimitiveType.PrimitiveTypeKind - Enum Class in dev.civl.mc.model.IF.type
civlProperty() - Method in exception class dev.civl.mc.log.IF.CIVLExecutionException
civlProperty() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
civlProperty() - Method in exception class dev.civl.mc.state.IF.CIVLStateException
CIVLProperty - Enum Class in dev.civl.mc.model.IF: Enum class for representing different properties that CIVL checks for.
CIVLRegularRangeType - Interface in dev.civl.mc.model.IF.type
CIVLREP - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The name of the directory into which CIVL will store the artifacts it generates.
CIVLScopeType - Interface in dev.civl.mc.model.IF.type: The $scope type in the CIVL-C language.
civlSetType(CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the CIVLSetType.
CIVLSetType - Interface in dev.civl.mc.model.IF.type: A CIVLType representing a set of a non-set kind CIVLType.
CIVLSource - Interface in dev.civl.mc.model.IF: A CIVLSource object represents a range of text in a source file.
CIVLStateException - Exception Class in dev.civl.mc.state.IF: Extends an execution exception with a state at which error occurred.
CIVLStateException(CIVLProperty, CIVLException.Certainty, String, State, CIVLSource) - Constructor for exception class dev.civl.mc.state.IF.CIVLStateException
CIVLStateManager - Class in dev.civl.mc.kripke.IF: StateManager extends StateManager for CIVL models.
CIVLStateManager() - Constructor for class dev.civl.mc.kripke.IF.CIVLStateManager
CIVLStatePredicate - Interface in dev.civl.mc.predicate.IF
CIVLStateType - Interface in dev.civl.mc.model.IF.type
CIVLStructOrUnionType - Interface in dev.civl.mc.model.IF.type: Represents a "record" type (i.e.
CIVLSyntaxException - Exception Class in dev.civl.mc.model.IF: An exception thrown when there is syntax error in the program being verified, e.g., calling $choose_int with more than one arguments, etc.
CIVLSyntaxException(String) - Constructor for exception class dev.civl.mc.model.IF.CIVLSyntaxException
CIVLSyntaxException(String, Source) - Constructor for exception class dev.civl.mc.model.IF.CIVLSyntaxException
CIVLSyntaxException(String, CIVLSource) - Constructor for exception class dev.civl.mc.model.IF.CIVLSyntaxException
CIVLSyntaxException(String, Sourceable) - Constructor for exception class dev.civl.mc.model.IF.CIVLSyntaxException
civlSystemFunction - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The name of the CIVL system function, which is the starting point of a CIVL model.
CIVLType - Interface in dev.civl.mc.model.IF.type: Parent of all types.
CIVLType.TypeKind - Enum Class in dev.civl.mc.model.IF.type
CIVLTypeFactory - Interface in dev.civl.mc.model.IF: The CIVL type factory provides the CIVL primitive types, like $bool, int, float, $scope , etc.
civlTypeOfObjByPointer(CIVLSource, State, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Computes the CIVL type of the object referring to by the given pointer.
CIVLUnimplementedFeatureException - Exception Class in dev.civl.mc.model.IF: An exception thrown when there is not necessarily anything wrong with the program begin verified, but some CIVL feature has not yet been implemented.
CIVLUnimplementedFeatureException(String) - Constructor for exception class dev.civl.mc.model.IF.CIVLUnimplementedFeatureException
CIVLUnimplementedFeatureException(String, Source) - Constructor for exception class dev.civl.mc.model.IF.CIVLUnimplementedFeatureException
CIVLUnimplementedFeatureException(String, CIVLSource) - Constructor for exception class dev.civl.mc.model.IF.CIVLUnimplementedFeatureException
CIVLUnimplementedFeatureException(String, Sourceable) - Constructor for exception class dev.civl.mc.model.IF.CIVLUnimplementedFeatureException
clause() - Method in interface dev.civl.mc.semantics.IF.Transition
clauses() - Method in interface dev.civl.mc.predicate.IF.AndPredicate: Returns all predicates contained by this And predicate.
clear() - Method in class dev.civl.mc.util.IF.SeqSet: Makes this set empty.
clear() - Method in class dev.civl.mc.util.IF.SeqSet.Node: Empties childrenIndexes.
clearAnonFragment() - Method in interface dev.civl.mc.model.IF.ModelFactory: Clear the current anonymous fragment.
clearDependsEvents() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: clears the depends events of this behavior.
clone() - Method in class dev.civl.mc.util.IF.SeqSet
CMON - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CMON_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CODE - Static variable in class dev.civl.mc.transform.IF.AnnotationTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.ComplexTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.ContractTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.Cuda2CIVLTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.GeneralTransformer
CODE - Static variable in class dev.civl.mc.transform.IF.IntOperationTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.IOTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.LoopContractTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.MPI2CIVLTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.OpenMP2CIVLTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.OpenMPSimplifier
CODE - Static variable in class dev.civl.mc.transform.IF.Pthread2CIVLTransformer: The code (short name) of this transformer.
CODE - Static variable in class dev.civl.mc.transform.IF.ShortCircuitTransformer
CodeAnalyzer - Interface in dev.civl.mc.analysis.IF: This represents a code analyzer for analyzing source code for a certain property.
codeAnalyzers() - Method in interface dev.civl.mc.model.IF.ModelFactory: The list of code analyzers associate with this model.
COLLATE_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
collator() - Method in interface dev.civl.mc.model.IF.statement.UpdateStatement
COLLECT_HEAPS - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COLLECT_OUTPUT - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COLLECT_PROCESSES - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COLLECT_SCOPES - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COLLECT_SYMBOLIC_CONSTANTS - Static variable in class dev.civl.mc.config.IF.CIVLConstants
collectedOutputs() - Method in class dev.civl.mc.kripke.IF.CIVLStateManager: Outputs collected for the model during the search.
collectHeaps() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
collectHeaps(State, Set<CIVLHeapException.HeapErrorKind>) - Method in interface dev.civl.mc.state.IF.StateFactory: Performs a garbage collection and canonicalization of heaps.
collectHeapsO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Collect heaps? true by default.
collectOutputO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Collect output? false by default.
collectOutputs() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
collectProcesses() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
collectProcesses(State) - Method in interface dev.civl.mc.state.IF.StateFactory: Performs a garbage collection and canonicalization of the process states.
collectProcessesO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Collect processes? true by default.
collectScopes() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
collectScopes(State, Set<CIVLHeapException.HeapErrorKind>) - Method in interface dev.civl.mc.state.IF.StateFactory: Performs a garbage collection and canonicalization of dynamic scopes.
collectScopesO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Collect scopes? true by default.
collectSymbolicConstantsO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Collect symbolic constants ? false by default.
collectSymbolicNames() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
coloredText(Utils.Color, String) - Static method in class dev.civl.mc.util.IF.Utils
combineWith(Fragment) - Method in interface dev.civl.mc.model.IF.Fragment: Combine two fragment in sequential order.
COMM - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COMM_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COMM_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of $comm type, which is the object type of the handle $comm.
COMM_WORLD - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the identifier of the MPI_Comm variable in the final CIVL program.
COMM2 - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COMMUNICATION - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
comparableExpression(Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Translates an expression to be of the type for comparable operations i.e.
compareTo(LogEntry) - Method in class dev.civl.mc.log.IF.CIVLLogEntry
complete() - Method in interface dev.civl.mc.model.IF.Model: Complete the model.
complete() - Method in interface dev.civl.mc.model.IF.Scope
complete(StructOrUnionField[]) - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Completes this struct type by specifying the fields as an array.
complete(SymbolicType, SymbolicArrayType) - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: complete the type information of the malloc statement.
complete(Collection<MallocStatement>, SymbolicType, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
complete(Collection<StructOrUnionField>) - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Completes this struct type by specifying the fields as a collection.
complete(List<CIVLType>, Collection<SymbolicType>, SymbolicUnionType) - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
COMPLETE_ARRAY - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
completeArrayType(CIVLType, Expression) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns a new complete array type with specified extent (length expression) and element type.
completeBundleType(CIVLBundleType, List<CIVLType>, Collection<SymbolicType>) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Completes the bundle type by specifying the list of all dynamic types which can occur as bundle elements.
completeDomainType(CIVLType, int) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Creates a complete regular domain type, which is has the given dimension and is composed by the given range type.
completeHeapType(CIVLHeapType, Collection<MallocStatement>) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Completes the heap type.
COMPLEX - Static variable in class dev.civl.mc.config.IF.CIVLConstants
ComplexTransformer - Class in dev.civl.mc.transform.IF
ComplexTransformer(ASTFactory) - Constructor for class dev.civl.mc.transform.IF.ComplexTransformer
COMPOSITE - Enum constant in enum class dev.civl.mc.model.IF.contract.DependsEvent.DependsEventKind
CompositeEvent - Interface in dev.civl.mc.model.IF.contract: This represents a composite event, which could be a union/difference/intersect of another two depends events.
CompositeEvent.CompositeEventOperator - Enum Class in dev.civl.mc.model.IF.contract
COMPOUND - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind
COMPOUND_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
compoundLiteralExpression(CIVLSource, Scope, CIVLType, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates a new instance of a compound literal expression.
CompoundLiteralExpression - Interface in dev.civl.mc.model.IF.expression: This class represents compound literal expressions, including string literals.
CompoundLiteralExpression.CIVLCompoundLiteralObject - Interface in dev.civl.mc.model.IF.expression: The CIVL model counterpart of CompoundLiteralObject in ABC.
CompoundLiteralExpression.CIVLLiteralObject - Interface in dev.civl.mc.model.IF.expression: The CIVL model counterpart of LiteralObject in ABC.
CompoundLiteralExpression.CIVLScalarLiteralObject - Interface in dev.civl.mc.model.IF.expression: The CIVL model counterpart of ScalarLiteralObject in ABC.
computeImpactScopeOfLocation(Location) - Method in interface dev.civl.mc.model.IF.ModelFactory: Computes the impact scope of a location, which is the highest scope that the location accesses.
computePathconditionOfLocations(ModelFactory) - Method in interface dev.civl.mc.model.IF.CIVLFunction
computeWritableVariables(Set<Variable>) - Method in interface dev.civl.mc.model.IF.location.Location
CONCRETE - Enum constant in enum class dev.civl.mc.model.IF.CIVLException.Certainty: A concrete trace verifies this is an error: the highest level of certainty that this represents a real error in the program being analyzed.
CONCURRENCY - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CONCURRENCY_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
COND - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind: Conditional expression c ? a : b, instance of ConditionalExpression
conditionalExpression(CIVLSource, Expression, Expression, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: The ternary conditional expression ("?" in C).
ConditionalExpression - Interface in dev.civl.mc.model.IF.expression: The ternary conditional expression ("?" in C).
consoleUpdatePeriod - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Number of seconds between printing of update messages.
CONSTANT_WRITE - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
constantValue() - Method in interface dev.civl.mc.model.IF.expression.Expression: The immutable constant value of this expression.
constantValue() - Method in interface dev.civl.mc.model.IF.variable.Variable: returns the constant value of this variable.
containingScope() - Method in interface dev.civl.mc.model.IF.CIVLFunction
contains(int...) - Method in class dev.civl.mc.util.IF.SeqSet: Does this set contain the set [s] of sequences which extend a given sequence s?
contains(Variable) - Method in interface dev.civl.mc.model.IF.Scope: If a variable is already included in this scope, return the included variable.
contains(MemoryUnit, MemoryUnit) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: Does mu1 contains mu2? returns true iff mu1 equals mu2, or mu1 and mu2 are referring to the same object and mu1 is containing mu2.
contains(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if the object that the container pointer points to contains that of the element pointer.
containsAll(SeqSet) - Method in class dev.civl.mc.util.IF.SeqSet: Does this set contain the given set?
containsHere() - Method in interface dev.civl.mc.model.IF.expression.Expression: checks if this expression contains the constant $here.
containsHere() - Method in interface dev.civl.mc.model.IF.statement.Statement: checks if the statement (including its guard) contains the constant $here.
containsVariable(String) - Method in interface dev.civl.mc.model.IF.Scope
continuity() - Method in interface dev.civl.mc.model.IF.AbstractFunction
CONTRACT - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.MPIModelKind
CONTRACT_CHECK_ALL - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Default option value for -mpiContract option CIVLConstants.mpiContractO
CONTRACT_CHECK_NONE - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Default option value for -mpiContract option CIVLConstants.mpiContractO
ContractFactory - Interface in dev.civl.mc.model.IF.contract: This factory is to create new instances of function contract components.
ContractMPICommRankName - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The extended "\mpi_comm_rank" constant used in CIVL-ACSL contracts which stands for the rank in a specific communicator of an MPI process.
ContractMPICommSizeName - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The extended "\mpi_comm_size" constant used in CIVL-ACSL contracts which stands for the number of MPI processes in a specific communicator.
ContractResultName - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The "\result" constant used in ACSL contracts which stands for the returned value.
ContractTransformer - Class in dev.civl.mc.transform.IF
ContractTransformer(ASTFactory, String, CIVLConfiguration) - Constructor for class dev.civl.mc.transform.IF.ContractTransformer
CONVERGE_W_MEM_EQ - Static variable in class dev.civl.mc.config.IF.CIVLConstants
convergeWithMemEquality() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
copyAs(CIVLPrimitiveType, SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLType
copyAs(CIVLPrimitiveType, SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.StructOrUnionField
count - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArraySlice: the number of elements in the slice
createCompoundLiteralObject(CIVLType, List<CompoundLiteralExpression.CIVLLiteralObject>) - Method in interface dev.civl.mc.model.IF.expression.CompoundLiteralExpression
createScalarLiteralObject(CIVLType, Expression) - Method in interface dev.civl.mc.model.IF.expression.CompoundLiteralExpression
CTYPE - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CUDA - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CUDA_RUNTIME_API - Static variable in class dev.civl.mc.config.IF.CIVLConstants
CUDA_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
Cuda2CIVLTransformer - Class in dev.civl.mc.transform.IF
Cuda2CIVLTransformer(ASTFactory) - Constructor for class dev.civl.mc.transform.IF.Cuda2CIVLTransformer
CYAN - Enum constant in enum class dev.civl.mc.util.IF.Utils.Color
CYCLES_VIOLATE - Static variable in class dev.civl.mc.config.IF.CIVLConstants

D

date - Static variable in class dev.civl.mc.config.IF.Version: The date of this release of CIVL.
Deadlock - Interface in dev.civl.mc.predicate.IF: An absolute deadlock occurs if all of the following hold: not every process has terminated no process has an enabled statement (note that a send statement is enabled iff the current number of buffered messages is less than the buffer bound).
DEADLOCK - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
deallocate(State, SymbolicExpression, SymbolicExpression, int, int) - Method in interface dev.civl.mc.state.IF.StateFactory: Deallocates a heap object from the heap of a given dyscope.
debug - Static variable in class dev.civl.mc.run.IF.UserInterface: Running in debug mode (which prints debugging information)?
debug() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
DEBUG - Static variable in class dev.civl.mc.config.IF.CIVLConstants
debugO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Debug option, false by default.
debugOrVerbose() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
DECOMP_ALL - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: ALL, corresponds to the enumerator ALL of the enumeration type $domain_decomposition.
DECOMP_RANDOM - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: RANDOM, corresponds to the enumerator ALL of the enumeration type $domain_decomposition.
DECOMP_ROUND_ROBIN - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: ROUND_ROBIN, corresponds to the enumerator ALL of the enumeration type $domain_decomposition.
decrementAtomicCount() - Method in interface dev.civl.mc.state.IF.ProcessState: Decrease the atomic block counter.
defaultBehavior() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: Returns the default behavior of the function.
definition() - Method in interface dev.civl.mc.model.IF.LogicFunction
degree() - Method in interface dev.civl.mc.model.IF.expression.DifferentiableExpression: The number of derivatives that exist and are continuous.
dependsAnyact() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Is this function depending on anything?
DependsEvent - Interface in dev.civl.mc.model.IF.contract: This represents an event which is used as one argument of the depends clause.
DependsEvent.DependsEventKind - Enum Class in dev.civl.mc.model.IF.contract
dependsEventKind() - Method in interface dev.civl.mc.model.IF.contract.DependsEvent: Returns the kind of this event.
dependsEvents() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the depends events of this behavior.
dependsNoact() - Method in interface dev.civl.mc.model.IF.CIVLFunction
dependsNoact() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Is this function depending on nothing?
deref() - Method in interface dev.civl.mc.model.IF.expression.MemoryUnitExpression: shall this memory unit be dereferenced?
dereference(CIVLSource, State, int, String, SymbolicExpression, boolean, boolean) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Given a pointer value, dereferences it in the given state to yield the symbolic expression value stored at the referenced location.
DEREFERENCE - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
DEREFERENCE - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
DEREFERENCE - Enum constant in enum class dev.civl.mc.model.IF.expression.LHSExpression.LHSExpressionKind
dereferenceExpression(CIVLSource, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Returns a new dereference expression (*p) with operand pointer.
DereferenceExpression - Interface in dev.civl.mc.model.IF.expression
DERIVATIVE - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
derivativeCallExpression(CIVLSource, AbstractFunction, List<Pair<Variable, IntegerLiteralExpression>>, List<Expression>) - Method in interface dev.civl.mc.model.IF.ModelFactory: An expression for a call to the derivative of an abstract function.
DerivativeCallExpression - Interface in dev.civl.mc.model.IF.expression: An uninterpreted call to the derivative of an abstract function.
dev.civl.mc - module dev.civl.mc
dev.civl.mc - package dev.civl.mc: The main package for CIVL, providing a command line interface and a class "CIVL" that invokes all the components in the CIVL tool chain to perform requested tasks.
dev.civl.mc.analysis.IF - package dev.civl.mc.analysis.IF: Module analysis provides a list of analyzers for static/runtime analyzing of a program.
dev.civl.mc.config.IF - package dev.civl.mc.config.IF: Module config provides static configurations of the CIVL tool.
dev.civl.mc.dynamic.IF - package dev.civl.mc.dynamic.IF: Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
dev.civl.mc.kripke.IF - package 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 - package dev.civl.mc.log.IF: Module log provides the data structure for logging errors during verification.
dev.civl.mc.model.IF - package 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 - package dev.civl.mc.model.IF.contract
dev.civl.mc.model.IF.expression - package dev.civl.mc.model.IF.expression: Submodule model.expression defines expression in CIVL.
dev.civl.mc.model.IF.expression.reference - package dev.civl.mc.model.IF.expression.reference
dev.civl.mc.model.IF.location - package 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 - package dev.civl.mc.model.IF.statement: Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.model.IF.type - package dev.civl.mc.model.IF.type: Submodule model.type defines types in CIVL.
dev.civl.mc.model.IF.variable - package dev.civl.mc.model.IF.variable: Submodule model.variable defines variables in CIVL.
dev.civl.mc.predicate.IF - package dev.civl.mc.predicate.IF: Module predicate defines predicates that are required to hold for any CIVL-C programs.
dev.civl.mc.run.IF - package dev.civl.mc.run.IF: Module run parses command line inputs and initializes the tool.
dev.civl.mc.semantics.IF - package dev.civl.mc.semantics.IF: Module semantics implements the semantics of CIVL-C.
dev.civl.mc.state.IF - package dev.civl.mc.state.IF: Module state is responsible for the creation and manipulation of states of a CIVL model.
dev.civl.mc.transform.IF - package dev.civl.mc.transform.IF: Module transform defines various kinds of transformations of an AST into a CIVL AST.
dev.civl.mc.util.IF - package dev.civl.mc.util.IF: Module util provides various general-purpose utilities used by CIVL.
DIFFERENCE - Enum constant in enum class dev.civl.mc.model.IF.contract.CompositeEvent.CompositeEventOperator
DIFFERENTIABLE - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
differentiableExpression(CIVLSource, AbstractFunction, int, Expression[], Expression[]) - Method in interface dev.civl.mc.model.IF.ModelFactory: An expression representing the claim that some function is differentiable.
DifferentiableExpression - Interface in dev.civl.mc.model.IF.expression: This expression encodes the claim that a real, abstract function is differentiable.
dimension() - Method in interface dev.civl.mc.model.IF.expression.DomainGuardExpression: Returns the dimension of the domain expression.
dimension() - Method in interface dev.civl.mc.model.IF.expression.RecDomainLiteralExpression: Returns the dimension of this domain literal, which is equal to the number of ranges.
dimension() - Method in interface dev.civl.mc.model.IF.statement.CivlParForSpawnStatement: returns the dimension of the domain
dimension() - Method in interface dev.civl.mc.model.IF.type.CIVLArrayType: computes the dimension of this array type.
dimensions - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArrayShape
DIRECT - Static variable in class dev.civl.mc.config.IF.CIVLConstants
direct0 - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Inject instrumentation to direct the branches at the line numbers in given file so as to explore a sub-space of execution.
directSymEx() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
DISABLE_LOCAL_BLOCK - Static variable in class dev.civl.mc.config.IF.CIVLConstants
disableLocalBlock() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
disableLocalBlockO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Disable the local block, which optimizes the POR impl.
disjoint(SeqSet) - Method in class dev.civl.mc.util.IF.SeqSet: Are this set and the given set disjoint?
DIVIDE - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
DIVISION_BY_ZERO - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
domain() - Method in interface dev.civl.mc.model.IF.expression.DomainGuardExpression: Returns the domain expression.
domain() - Method in interface dev.civl.mc.model.IF.statement.CivlParForSpawnStatement: returns the domain according to which processes will be spawned.
domain() - Method in interface dev.civl.mc.model.IF.statement.DomainIteratorStatement: Returns the iteration domain expression, which is the expression following the colon.
DOMAIN - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind
DOMAIN - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
DOMAIN - Static variable in class dev.civl.mc.config.IF.CIVLConstants
DOMAIN_GUARD - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
DOMAIN_ITERATOR - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind: CIVL for loop ($for) enter statement
domainGuard(CIVLSource, List<Variable>, Variable, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: 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.
DomainGuardExpression - Interface in dev.civl.mc.model.IF.expression: This is the guard expression of CIVL for loops ($for).
DomainIteratorStatement - Interface in dev.civl.mc.model.IF.statement: Updates the loop variables with the next element of a domain.
domainType(CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: This returns the universal domain type ($domain).
domSizeVar() - Method in interface dev.civl.mc.model.IF.statement.CivlParForSpawnStatement: returns the variable that represents the size of the domain, i.e., how many elements are contained in the domain.
domSizeVariable(CIVLSource, Scope) - Method in interface dev.civl.mc.model.IF.ModelFactory
DOT - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
DOT - Enum constant in enum class dev.civl.mc.model.IF.expression.LHSExpression.LHSExpressionKind
dotExpression(CIVLSource, Expression, int) - Method in interface dev.civl.mc.model.IF.ModelFactory: A dot expression is a reference to a struct field.
DotExpression - Interface in dev.civl.mc.model.IF.expression: A dot expression is a reference to a field in a struct or union.
DOUBLE - Enum constant in enum class dev.civl.mc.semantics.IF.Format.ConversionType
DOUBLE_COMPLEX_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The CIVL-C struct type corresponding to C's double _Complex.
DPOR - Static variable in class dev.civl.mc.config.IF.CIVLConstants
dporEnabled() - Method in class dev.civl.mc.config.IF.CIVLConfiguration: Returns whether we are using dynamic partial order reduction
dporO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Specifies whether to use DPOR algorithm for model checking.
DYNAMIC - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind
DYNAMIC_CONSTANT_SCOPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
DYNAMIC_NULL_SCOPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
DYNAMIC_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the name of $dynamic type
DYNAMIC_TYPE_NAME - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: name of the symbolic type for mapping user-defined types to integers
DYNAMIC_TYPE_OF - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
DYNAMIC_UNDEFINED_SCOPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
DynamicMemoryLocationSet - Interface in dev.civl.mc.dynamic.IF: This class is a immutable data structure that stores a set of memory locations.
DynamicMemoryLocationSetFactory - Interface in dev.civl.mc.dynamic.IF
dynamicMemType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory
Dynamics - Class in dev.civl.mc.dynamic.IF: Entry point of the module dynamic.
Dynamics() - Constructor for class dev.civl.mc.dynamic.IF.Dynamics
DynamicScope - Interface in dev.civl.mc.state.IF: A DynamicScope is a runtime instance of a static scope.
dynamicSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the symbolic type used to represent values of type CIVLDynamicType
dynamicType() - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: returns the symbolic type of dynamic type which is used to model user-defined types.
dynamicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get the dynamic type.
dynamicTypeOfExpression(CIVLSource, CIVLType) - Method in interface dev.civl.mc.model.IF.ModelFactory: Returns a "DynamicTypeOf" expression with the given type argument.
DynamicTypeOfExpression - Interface in dev.civl.mc.model.IF.expression: A "DynamicTypeOf" expression.
dynamicTypeOfObjByPointer(CIVLSource, State, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Computes the SymbolicType of the object referring to by the given pointer.
dyscopeID() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
dyscopeID() - Method in interface dev.civl.mc.state.IF.MemoryUnit: The ID of the dynamic scope of the memory unit.
dyscopeName() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException

E

elaborateDomainPointer() - Method in interface dev.civl.mc.model.IF.ModelFactory
ELEMENT - Enum constant in enum class dev.civl.mc.model.IF.expression.reference.ArraySliceReference.ArraySliceKind
elementType() - Method in interface dev.civl.mc.model.IF.type.CIVLArrayType
elementType() - Method in interface dev.civl.mc.model.IF.type.CIVLSetType
empty() - Method in interface dev.civl.mc.dynamic.IF.DynamicMemoryLocationSetFactory
emptyState(int) - Method in interface dev.civl.mc.state.IF.StateFactory: Creates an empty state which contains no dyscopes but an array of process states with length 'nprocs'.
ENABLE_PRINTF - Static variable in class dev.civl.mc.config.IF.CIVLConstants
enabledTransitions(State, CallOrSpawnStatement, BooleanExpression, int) - Method in interface dev.civl.mc.kripke.IF.LibraryEnabler: Computes the enabled transitions of a given function call.
enablePrintf() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
enablePrintfO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Enables printf? true by default.
Enabler - Interface in dev.civl.mc.kripke.IF: Enabler extends EnablerIF for CIVL models.
enclosingType() - Method in interface dev.civl.mc.model.IF.type.StructOrUnionField
ensurances() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the postconditions of this behavior.
ENSURES - Enum constant in enum class dev.civl.mc.model.IF.contract.FunctionContract.ContractKind
enterAtomic() - Method in interface dev.civl.mc.model.IF.location.Location: Check if the location is entering a general atomic block.
enterAtomic() - Method in interface dev.civl.mc.model.IF.statement.AtomicLockAssignStatement
enterAtomic(State, int) - Method in interface dev.civl.mc.state.IF.StateFactory: Process pid enters a new atomic section.
ENUM - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
enumType(String, Map<String, BigInteger>) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Creates a new instance of enumeration type with the specified name.
EOS - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The int value of the char '\0', which represents the end of string.
EQUAL - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
equals(Object) - Method in class dev.civl.mc.log.IF.CIVLLogEntry
equals(Object) - Method in class dev.civl.mc.util.IF.Pair
equals(Object) - Method in class dev.civl.mc.util.IF.SeqSet: Do this set and the given set represent the same set of sequences?
equals(Object) - Method in class dev.civl.mc.util.IF.Triple
equalsWork(DependsEvent) - Method in interface dev.civl.mc.model.IF.contract.DependsEvent: Does this event equals to that event?
err() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
ERRNO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
ERROR_BOUND - Static variable in class dev.civl.mc.config.IF.CIVLConstants
ERROR_STATE_EQUIV - Static variable in class dev.civl.mc.config.IF.CIVLConstants
errorBoundO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The maximal number of errors allowed before terminating CIVL.
errorLogger() - Method in interface dev.civl.mc.semantics.IF.Evaluator: Returns the error logger object of this evaluator.
errorLogger() - Method in interface dev.civl.mc.semantics.IF.Executor: Returns the error logger used by this executor.
errorStateEquiv() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
errorStateEquivO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The semantics for used to determine when error states are equivalent; CIVL suppresses logging of equivalent states.
evaluate(State, int, Expression) - Method in interface dev.civl.mc.semantics.IF.Evaluator
evaluate(State, int, Expression, boolean) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluates the expression and returns the result, which is a symbolic expression value.
evaluateCastWorker(State, int, String, CIVLType, Expression) - Method in interface dev.civl.mc.semantics.IF.Evaluator
evaluateCIVLArrayType(State, int, CIVLArrayType) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluating the symbolic array type from a CIVLArrayType based on current state and specific process.
evaluateFunctionIdentifier(State, int, Expression, CIVLSource) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluates a function pointer expression.
evaluateGuard(CIVLSource, State, int, String, Expression[]) - Method in interface dev.civl.mc.semantics.IF.LibraryEvaluator: Evaluates the guard of a system function.
evaluateMemoryUnit(State, Pair<Scope, SymbolicExpression[]>, int, Expression) - Method in interface dev.civl.mc.semantics.IF.MemoryUnitExpressionEvaluator: Evaluates the memory unit represented by an expression in a contract.
evaluatePointerAdd(State, int, BinaryExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluates pointer addition.
evaluates(State, int, MemoryUnitExpression, MemoryUnitSet) - Method in interface dev.civl.mc.semantics.IF.MemoryUnitExpressionEvaluator: evaluates the static impact memory unit expression which is the result of static analysis
evaluateSizeofType(CIVLSource, State, int, CIVLType) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluate the size of a CIVL type.
Evaluation - Class in dev.civl.mc.semantics.IF: Represents the result of evaluating an expression in two parts: the (possibly) new state resulting from side-effects arising from the evaluation, and the value resulting from the evaluation.
Evaluation(State, SymbolicExpression) - Constructor for class dev.civl.mc.semantics.IF.Evaluation: Creates a new instance of evaluation.
evaluator - Static variable in class dev.civl.mc.util.IF.BranchConstraints
evaluator() - Method in interface dev.civl.mc.semantics.IF.Executor
evaluator() - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer
Evaluator - Interface in dev.civl.mc.semantics.IF: This is the CIVL main evaluator.
execute(State, int, CallOrSpawnStatement, String) - Method in interface dev.civl.mc.semantics.IF.LibraryExecutor: Executes the given call statement for a certain process at the given state.
execute(State, int, Transition) - Method in interface dev.civl.mc.semantics.IF.Executor: Returns the state that results from executing the statement, or null if path condition becomes unsatisfiable.
execute_printf(CIVLSource, State, int, String, Expression[], SymbolicExpression[], boolean) - Method in interface dev.civl.mc.semantics.IF.Executor
Executor - Interface in dev.civl.mc.semantics.IF
EXISTS - Enum constant in enum class dev.civl.mc.model.IF.expression.QuantifiedExpression.Quantifier
expression() - Method in interface dev.civl.mc.model.IF.expression.ArrayLambdaExpression: The expression e(x).
expression() - Method in interface dev.civl.mc.model.IF.expression.QuantifiedExpression: The expression e(x).
expression() - Method in interface dev.civl.mc.model.IF.statement.NoopStatement
expression() - Method in interface dev.civl.mc.model.IF.statement.ReturnStatement
Expression - Interface in dev.civl.mc.model.IF.expression: The parent of all expressions.
Expression.ExpressionKind - Enum Class in dev.civl.mc.model.IF.expression
expressionEvaluation(State, int, Expression, boolean) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Compute a friendly string representation of an expression's evaluation.
expressionKind() - Method in interface dev.civl.mc.model.IF.expression.Expression: Returns the kind of this expression
expressionOfType(CIVLType, SymbolicType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Given a symbolic type, returns a canonical symbolic expression which somehow wraps that type so it can be used as a value.
expressionScope() - Method in interface dev.civl.mc.model.IF.expression.Expression
EXTENDED_QUANTIFIER - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
extendedQuantifiedExpression(CIVLSource, CIVLType, ExtendedQuantifiedExpressionNode.ExtendedQuantifier, Expression, Expression, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory
ExtendedQuantifiedExpression - Interface in dev.civl.mc.model.IF.expression: The representation for the "fold expression" in ACSL, e.g.
extendedQuantifier() - Method in interface dev.civl.mc.model.IF.expression.ExtendedQuantifiedExpression: returns the quantifier of this expression
extendPointer(SymbolicExpression, ReferenceExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: * Constructs a pointer by combining a pointer to a component, either an object (a heap atomic object or a normal object) or a sub-component of an object, and a reference expression w.r.t that component.
extendReference(MemoryUnit, ReferenceExpression) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: extends a memory unit with extra references.
extendToFull(ValueSetReference, SymbolicType) - Method in interface dev.civl.mc.dynamic.IF.ValueSetUtility: Extends the ValueSetReference vsRef to an equivalent set of references to primitives
extent() - Method in interface dev.civl.mc.model.IF.type.CIVLCompleteArrayType
extents - Variable in class dev.civl.mc.semantics.IF.ArrayToolBox.ArrayShape
externVariables() - Method in interface dev.civl.mc.model.IF.Model
extractArrayIndicesFrom(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Given a pointer to an array element, returns the indices of the element.
extractArraySlice(ArrayToolBox.ArraySlice) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox: Returns a SymbolicExpression representing the given ArrayToolBox.ArraySlice.
extractInt(CIVLSource, NumericExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Gets a Java concrete int from a symbolic expression
extractIntField(CIVLSource, SymbolicExpression, IntObject) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Gets a concrete Java int from the field of a symbolic expression of tuple type or throws exception.

F

factory() - Method in interface dev.civl.mc.model.IF.Model
factory() - Method in interface dev.civl.mc.model.IF.ModelBuilder
FAIR - Static variable in class dev.civl.mc.config.IF.CIVLConstants
fairO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: If this is true, and termination is being checked, then a cycle in which some process remains enabled at each state will not be considered a violation of non-termination (as it is not considered to represent a real execution).
FENV - Static variable in class dev.civl.mc.config.IF.CIVLConstants
fid() - Method in interface dev.civl.mc.model.IF.CIVLFunction: The id of this function in its containing scope
fieldIndex() - Method in interface dev.civl.mc.model.IF.expression.DotExpression
fieldIndex() - Method in interface dev.civl.mc.model.IF.expression.reference.StructOrUnionFieldReference: The field index of this reference.
fields() - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Returns an iterable object over all the fields of this struct/union type, in ascending order.
FILE_STREAM_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The file reference type FILE.
FILE_SYSTEM_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the file system variable, created when stdio transformation is performed.
FILESYSTEM - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
finalStatements() - Method in interface dev.civl.mc.model.IF.Fragment
first - Variable in class dev.civl.mc.util.IF.Triple
firstValue() - Method in interface dev.civl.mc.model.IF.type.CIVLEnumType
FLOAT - Static variable in class dev.civl.mc.config.IF.CIVLConstants
FLOAT_COMPLEX_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The CIVL-C struct type corresponding to C's float _Complex.
FORALL - Enum constant in enum class dev.civl.mc.model.IF.expression.QuantifiedExpression.Quantifier
Format - Class in dev.civl.mc.semantics.IF
Format(StringBuffer, Format.ConversionType) - Constructor for class dev.civl.mc.semantics.IF.Format
Format.ConversionType - Enum Class in dev.civl.mc.semantics.IF
FORTRAN_ARRAY - Static variable in class dev.civl.mc.config.IF.CIVLConstants
FORTRAN_ARRAY_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
FORTRAN_SIGP - Static variable in class dev.civl.mc.config.IF.CIVLConstants
FORTRAN_SIGP_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
Fragment - Interface in dev.civl.mc.model.IF: A fragment is a sequence of statements.
freeVariable() - Method in interface dev.civl.mc.model.IF.expression.LambdaExpression: TODO: shouldn't this be called the "bound variable"? It is the opposite of free.
freeVariables() - Method in interface dev.civl.mc.model.IF.expression.Expression: Computes the set of variables which occur freely in this expression.
freeVariables() - Method in interface dev.civl.mc.model.IF.statement.Statement: Returns all free (not bound) variables that are referenced in this statement.
freeVariables() - Method in interface dev.civl.mc.model.IF.type.CIVLType
freshBoundVariableFor(SymbolicType, SymbolicExpression...) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Creating a bound variable of the given "type", which is an instance of SymbolicConstant, whose name has no conflict with any other symbolic constants in the given set of "expressions".
freshBoundVariablesFor(int, SymbolicType, SymbolicExpression...) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility
FULL - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.ErrorStateEquivalence
FUNC_CALL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind: instance of FunctionCallExpression
function() - Method in interface dev.civl.mc.model.IF.contract.CallEvent: The function (i.e., the callee) of this call event.
function() - Method in interface dev.civl.mc.model.IF.expression.AbstractFunctionCallExpression
function() - Method in interface dev.civl.mc.model.IF.expression.DifferentiableExpression: The function that is claimed to be differentiable.
function() - Method in interface dev.civl.mc.model.IF.expression.ExtendedQuantifiedExpression: returns the function
function() - Method in interface dev.civl.mc.model.IF.expression.FunctionIdentifierExpression
function() - Method in interface dev.civl.mc.model.IF.expression.SystemGuardExpression: The invoked function.
function() - Method in interface dev.civl.mc.model.IF.location.Location
function() - Method in interface dev.civl.mc.model.IF.Scope
function() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement: TODO: get rid of it
function() - Method in interface dev.civl.mc.model.IF.statement.UpdateStatement
function(CIVLSource, boolean, Identifier, Scope, List<Variable>, CIVLType, Scope, Location) - Method in interface dev.civl.mc.model.IF.ModelFactory: Create a new function.
function(String) - Method in interface dev.civl.mc.model.IF.Model: Get a function based on its name.
FUNCTION - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
FUNCTION_GUARD - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
FUNCTION_IDENTIFIER - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
FUNCTIONAL_EQUIVALENCE - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
FunctionalEquivalence - Interface in dev.civl.mc.predicate.IF: A functional equivalence predicate contains a specification output, which is a set of pairs (pathcondition, output variable map), and is checked at the final state of the program.
FunctionBehavior - Interface in dev.civl.mc.model.IF.contract: This represents a non-named behavior of the ACSL function contract.
functionCallExpression(CallOrSpawnStatement) - Method in interface dev.civl.mc.model.IF.ModelFactory: creates a system function call expression
FunctionCallExpression - Interface in dev.civl.mc.model.IF.expression
functionContract() - Method in interface dev.civl.mc.model.IF.CIVLFunction: returns the contract specification of this function.
FunctionContract - Interface in dev.civl.mc.model.IF.contract: This represents a block of ACSL contract for a function.
FunctionContract.ContractKind - Enum Class in dev.civl.mc.model.IF.contract: ContractKind: This kind is used to denotes all kinds of contracts.
functionExpression() - Method in interface dev.civl.mc.model.IF.expression.FunctionGuardExpression: Returns the function expression of the corresponding call statement of this guard expression.
functionExpression() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement
functionGuardExpression(CIVLSource, Expression, List<Expression>) - Method in interface dev.civl.mc.model.IF.ModelFactory
FunctionGuardExpression - Interface in dev.civl.mc.model.IF.expression: A function guard expression is the guard expression of a function call with a function pointer.
functionIdentifierExpression(CIVLSource, CIVLFunction) - Method in interface dev.civl.mc.model.IF.ModelFactory: creates a function identifier expression.
FunctionIdentifierExpression - Interface in dev.civl.mc.model.IF.expression
functionName() - Method in interface dev.civl.mc.model.IF.Scope
functionPointerSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Gets the symbolic function pointer type.
functions() - Method in interface dev.civl.mc.model.IF.Model
functionType() - Method in interface dev.civl.mc.model.IF.CIVLFunction: returns the type of this function.
functionType(CIVLType, CIVLType[]) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Creates a new instance of function type, which contains a return type and a list of parameter types.

G

GBARRIER_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of __gbarrier__ type, which is the object type of the handle $gbarrier.
GCOMM_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of __gcomm__ type, which is the object type of the handle $gcomm.
GCOMM_WORLD - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the identifier of the CMPI_Gcomm variable in the final CIVL program.
GCOMMS - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the identifier of the CMPI_Gcomm sequence variable in the final CIVL-MPI program
GD - Static variable in class dev.civl.mc.config.IF.CIVLConstants
GD_IO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
GDFX - Static variable in class dev.civl.mc.config.IF.CIVLConstants
GENERAL_ROOT - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
GeneralTransformer - Class in dev.civl.mc.transform.IF
GeneralTransformer(ASTFactory) - Constructor for class dev.civl.mc.transform.IF.GeneralTransformer
getAbsoluteFilePath() - Method in interface dev.civl.mc.model.IF.CIVLSource
getAbstractFunctionName(SymbolicUniverse, String) - Static method in class dev.civl.mc.model.IF.ModelConfiguration: Returns a StringObject which is the name of the value an abstract function.
getAbstractGuardOfFunctionCall(String, String, SymbolicExpression[]) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: returns the abstract guard of a function call
getAccessesAtomicFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction
getAllConfigurableProperties() - Static method in enum class dev.civl.mc.model.IF.CIVLProperty
getAllLibFilenames() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getAllLibHeaders() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getAllLibSrcs() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getAllLogicFunctions() - Method in interface dev.civl.mc.model.IF.Model
getAllOptions() - Static method in class dev.civl.mc.config.IF.CIVLConstants: Returns all options defined for CIVL in alphabetic order.
getAllUnconfigurableProperties() - Static method in enum class dev.civl.mc.model.IF.CIVLProperty
getAnalyzers(CIVLConfiguration, SymbolicUniverse) - Static method in class dev.civl.mc.analysis.IF.Analysis: gets all code analyzers as required in the configuration.
getAnnotationTransformerRecord() - Method in class dev.civl.mc.transform.IF.TransformerFactory
getArgument() - Method in interface dev.civl.mc.model.IF.expression.SizeofExpression
getArrayBaseType(State, CIVLSource, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: 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
getArrayIndex(CIVLSource, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Given a pointer to a certain element of some array, returns the index of the element that the pointer points to.
getAtomicLock(State, int) - Method in interface dev.civl.mc.state.IF.StateFactory: Declares that the process with the given PID now owns the atomic lock.
getAtomicSteps() - Method in interface dev.civl.mc.kripke.IF.TraceStep: Returns the list of atomic steps of this trace step.
getAttribute() - Method in interface dev.civl.mc.model.IF.AbstractFunction
getBehavior(String) - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: returns the behavior with the given name; null if no such behavior exists.
getCastType() - Method in interface dev.civl.mc.model.IF.expression.CastExpression
getCheckedPropertiesSummary() - Method in class dev.civl.mc.config.IF.CIVLConfiguration: Generates a summary of all CIVLProperty's that are enabled
getCivlLibHeaders() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getCivlLibSrcs() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getComplexTransformerRecord() - Method in class dev.civl.mc.transform.IF.TransformerFactory
getCondition() - Method in interface dev.civl.mc.model.IF.expression.ConditionalExpression
getConjunctiveClauses(BooleanExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the sub-clauses of a CNF clause.
getConstantValue() - Method in interface dev.civl.mc.model.IF.LogicFunction
getContent() - Method in interface dev.civl.mc.model.IF.CIVLSource
getContractTransformerRecord(String, CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getCStdLibHeaders() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getCStdLibSrcs() - Static method in class dev.civl.mc.config.IF.CIVLConstants
getCuda2CIVLTransformerRecord() - Method in class dev.civl.mc.transform.IF.TransformerFactory
getDimension() - Method in interface dev.civl.mc.model.IF.type.CIVLCompleteDomainType
getDimensionOf(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the dimension of the given domain.
getDomainElementType(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Get the type of elements of domain which are also elements of literal domain object.
getDomainInit(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Get the first integer tuple of a domain.
getDomainIterator(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Return a iterator for a domain object.
getDomainSize(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Computes the size of a domain, that is the number of elements contained in the domain.
getDynamicElementType() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: This returns the dynamic (symbolic type) corresponding to the static element type.
getDynamicObjectType() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: The object is the thing that is allocated; it is an array of some number of elements of the specified type.
getDynamicSubTypesUnion(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLDomainType: Since the domain type has couple more precise sub-types which are all in one union.
getDynamicType(State, int, CIVLType, CIVLSource, boolean) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluates the dynamic type of a given CIVL type at a certain state.
getDynamicType(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
getDynamicType(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLType: This returns the dynamic type corresponding to this static type in which all array extent expressions are ignored, i.e., all of the dynamic array types are incomplete.
getDynamicTypeIndex() - Method in interface dev.civl.mc.model.IF.type.CIVLType: All dynamic types occurring in a model are indexed.
getDyscope(int) - Method in interface dev.civl.mc.state.IF.State: Returns the id-th dynamic scope in this state.
getDyscope(int, int) - Method in interface dev.civl.mc.state.IF.State: Given a PID and a static scope ID , returns the ID of the first dyscope corresponding to the static scope and reachable from the given process.
getDyscope(int, Scope) - Method in interface dev.civl.mc.state.IF.State: Given a PID and a static scope, returns the ID of the first dyscope corresponding to the static scope and reachable from the given process.
getDyscopeId() - Method in interface dev.civl.mc.state.IF.ProcessState: The ID of the dynamic scope of the top frame on the call stack.
getDyscopeId(SymbolicExpression) - Method in interface dev.civl.mc.state.IF.StateFactory: Converts a value of scope type to a dynamic scope ID.
getDyscopeID(int, Variable) - Method in interface dev.civl.mc.state.IF.State: Given a process ID and a variable, finds the first dyscope containing the variable in the path starting from the dyscope of the current (top) frame of the process call stack and following the parent edges of the dyscope tree.
getElementType(int) - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
getExpression() - Method in interface dev.civl.mc.model.IF.expression.CastExpression
getExpression() - Method in interface dev.civl.mc.model.IF.expression.CompoundLiteralExpression.CIVLScalarLiteralObject
getExpressionType() - Method in interface dev.civl.mc.model.IF.expression.ArrayLambdaExpression
getExpressionType() - Method in interface dev.civl.mc.model.IF.expression.Expression
getExpressionType() - Method in interface dev.civl.mc.model.IF.expression.LambdaExpression
getExpressionType() - Method in interface dev.civl.mc.model.IF.expression.RealLiteralExpression: Returns the real type.
getFacts() - Method in interface dev.civl.mc.model.IF.type.CIVLPrimitiveType: Returns facts about this primitive type that should be added to the path condition whenever it is used.
getFalseBranch() - Method in interface dev.civl.mc.model.IF.expression.ConditionalExpression
getField(int) - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Returns the index-th field of this struct or union type.
getFieldIndex() - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression
getFieldIndex(String) - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType
getFileName() - Method in interface dev.civl.mc.model.IF.CIVLSource
getFinalState() - Method in interface dev.civl.mc.kripke.IF.TraceStep
getFreshSymbol(State, int, SymbolicType) - Method in interface dev.civl.mc.state.IF.StateFactory: Creates a fresh symbolic constant of the given type at the given state.
getFunction(int) - Method in interface dev.civl.mc.model.IF.Scope
getFunction(Identifier) - Method in interface dev.civl.mc.model.IF.Scope
getFunction(String) - Method in interface dev.civl.mc.model.IF.Scope
getFunctionConstantName(SymbolicUniverse, String) - Static method in class dev.civl.mc.model.IF.ModelConfiguration: Returns a StringObject which is the name of a function type symbolic constant.
getGeneralTransformerRecord() - Method in class dev.civl.mc.transform.IF.TransformerFactory
getGuard(Statement, int, State) - Method in interface dev.civl.mc.kripke.IF.Enabler: Computes the guard of a statement.
getHeapFieldId(CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the type of the heap field of the given index.
getHideConstant() - Method in interface dev.civl.mc.model.IF.ModelFactory
getHigh() - Method in interface dev.civl.mc.model.IF.expression.RegularRangeExpression: Returns the upper bound argument hi.
getHighOfRegularRange(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the upper bound of the given range.
getIncoming(int) - Method in interface dev.civl.mc.model.IF.location.Location
getIndexOf(SymbolicType) - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
getInitialValue() - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
getIntBit() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
getIntOperationTransformerRecord(Map<String, String>, CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getInvalidName(SymbolicUniverse) - Static method in class dev.civl.mc.model.IF.ModelConfiguration
getIOTransformerRecord(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getLeafNodeReference(State, SymbolicExpression, CIVLSource) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: 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.
getLeaves() - Method in class dev.civl.mc.util.IF.SeqSet
getLhs() - Method in interface dev.civl.mc.model.IF.statement.AssignStatement
getLHS() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: Returns the expression on the left-hand side of the assignment.
getLibrary() - Method in interface dev.civl.mc.model.IF.SystemFunction
getLibraryEnabler(String, Enabler, Evaluator, ModelFactory, SymbolicUtility, SymbolicAnalyzer) - Method in interface dev.civl.mc.kripke.IF.LibraryEnablerLoader: Obtains the library executor of the given name.
getLibraryEvaluator(String, Evaluator, ModelFactory, SymbolicUtility, SymbolicAnalyzer) - Method in interface dev.civl.mc.semantics.IF.LibraryEvaluatorLoader: Obtains the library evaluator of the given name.
getLibraryExecutor(String, Executor, ModelFactory, SymbolicUtility, SymbolicAnalyzer) - Method in interface dev.civl.mc.semantics.IF.LibraryExecutorLoader: Obtains the library executor of the given name.
getLiteralDomCounter() - Method in interface dev.civl.mc.model.IF.expression.DomainGuardExpression: The counter variable for iterating a literal domain step by step.
getLiteralDomCounter() - Method in interface dev.civl.mc.model.IF.statement.DomainIteratorStatement: Returns a counter variable used for iterating on a literal domain step by step.
getLiteralDomCounterIdentifier(CIVLSource, int) - Method in interface dev.civl.mc.model.IF.ModelFactory: Get the name of the counter variable for the for loop on a literal domain
getLiteralObject() - Method in interface dev.civl.mc.model.IF.expression.CompoundLiteralExpression
getLocation() - Method in interface dev.civl.mc.model.IF.CIVLSource: Returns location information only (not actual source text).
getLocation() - Method in interface dev.civl.mc.state.IF.ProcessState: Returns the location at the top of the call stack of this process.
getLoopContract() - Method in interface dev.civl.mc.model.IF.statement.LoopBranchStatement: Returns an instance of LoopContract if LoopBranchStatement.isContracted() returns true, otherwise, returns null.
getLoopContractTransformerRecord(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getLow() - Method in interface dev.civl.mc.model.IF.expression.RegularRangeExpression: Returns the lower bound argument lo.
getLowOfRegularRange(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the lower bound of the given range.
getMalloc(int) - Method in interface dev.civl.mc.model.IF.Model
getMalloc(int) - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
getMallocId() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: The malloc statements in the model are indexed, so each has unique ID number.
getMallocID(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: The parameter "pointer" must be a returned value of SymbolicUtility.heapMemUnit(SymbolicExpression)
getMaxProcs() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
getMemValue() - Method in interface dev.civl.mc.dynamic.IF.DynamicMemoryLocationSet
getMessage() - Method in exception class dev.civl.mc.semantics.IF.LibraryLoaderException
getMPI2CIVLTransformerRecord() - Method in class dev.civl.mc.transform.IF.TransformerFactory
getName() - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
getNextInRectangularDomain(SymbolicExpression, List<SymbolicExpression>, int) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Get the subsequence of the given element of the domain.
getNumAtomicSteps() - Method in interface dev.civl.mc.kripke.IF.TraceStep: Returns the number of atomic steps contained in this trace step.
getNumIncoming() - Method in interface dev.civl.mc.model.IF.location.Location
getNumMallocs() - Method in interface dev.civl.mc.model.IF.Model
getNumMallocs() - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
getNumOutgoing() - Method in interface dev.civl.mc.model.IF.location.Location
getNumStateInstances() - Method in class dev.civl.mc.kripke.IF.CIVLStateManager: Returns the number of objects of type State that have been instantiated since this JVM started.
getNumStateInstances() - Method in interface dev.civl.mc.state.IF.StateFactory: Returns the number of objects of type State that have been instantiated since this JVM started.
getNumSteps() - Method in interface dev.civl.mc.semantics.IF.Executor: Returns the number of "steps" executed since this Executor was created.
getNumTypes() - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
getOpenMP2CIVLTransformer(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getOpenMP2CIVLTransformerRecord(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getOpenMPSimplifier(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getOpenMPSimplifierRecord(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory
getOption() - Method in enum class dev.civl.mc.model.IF.CIVLProperty
getOutgoing(int) - Method in interface dev.civl.mc.model.IF.location.Location
getOutputValues(String[]) - Method in interface dev.civl.mc.state.IF.State: Returns value of the output variables in the order of the given list of output names.
getParent() - Method in interface dev.civl.mc.state.IF.DynamicScope: Returns the dyscope ID of the parent of this dynamic scope in the dyscope tree.
getParentId(int) - Method in interface dev.civl.mc.state.IF.State: Gets the dynamic scope ID (dyscope ID) of the parent of the dynamic scope with the given dyscope ID.
getPartialPathConditions() - Method in interface dev.civl.mc.state.IF.ProcessState
getPathCondition(SymbolicUniverse) - Method in interface dev.civl.mc.state.IF.State: Returns the path condition.
getPermanentPathCondition() - Method in interface dev.civl.mc.state.IF.State: Returns the path condition, excluding the partial path conditions held by the process states.
getPid() - Method in interface dev.civl.mc.state.IF.ProcessState: Returns the process ID (pid) of this process state.
getPointer2MemoryBlock(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Takes a pointer to some location inside a memory block m, returns the pointer to m, where a memory block is defined as a space in heap which is allocated by once execution of $malloc.
getPossibleValidConsequences() - Method in interface dev.civl.mc.model.IF.CIVLFunction: Possible valid consequence is a valid contract expression which is POSSIBLE a consequence of the whole contract Notice that consequences only come from requirements
getPostState() - Method in interface dev.civl.mc.kripke.IF.AtomicStep: Returns the resulting state of this atomic step.
getProcBound() - Method in class dev.civl.mc.config.IF.CIVLConfiguration: returns the maximal number of processes allowed in a state.
getProcessId(SymbolicExpression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Translate a symbolic process id into an integer.
getProcessState(int) - Method in interface dev.civl.mc.state.IF.State: Returns the process state for the pid-th process.
getProcessStates() - Method in interface dev.civl.mc.state.IF.State: Returns the set of process states as an Iterable.
getPropertyTitle() - Method in enum class dev.civl.mc.model.IF.CIVLProperty
getPthread2CIVLTransformerRecord() - Method in class dev.civl.mc.transform.IF.TransformerFactory
getRangeOfRectangularDomain(SymbolicExpression, int) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the given index-th range of a rectangular domain.
getReachableMemUnitsWoPointer() - Method in interface dev.civl.mc.state.IF.ProcessState
getReachableMemUnitsWtPointer() - Method in interface dev.civl.mc.state.IF.ProcessState
getReachers() - Method in interface dev.civl.mc.state.IF.DynamicScope: Returns the reachers field.
getRegion() - Method in interface dev.civl.mc.model.IF.type.CIVLPointerType: Returns the highest scope in the static scope hierarchy in which the target of this pointer could be declared.
getScopeExpression() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: The first argument to the $malloc function is an expression of type pointer-to-heap.
getScopeValue(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Given a pointer value, returns the dynamic scope type component of that pointer value.
getShortCircuitTransformerRecord(CIVLConfiguration) - Method in class dev.civl.mc.transform.IF.TransformerFactory: Creates a new instance of a ShortCircuitTransformer
getSizeExpression() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: The second argument to the $malloc function is an integer expression specifying the size (number of bytes) to malloc.
getSizeof() - Method in interface dev.civl.mc.model.IF.type.CIVLPrimitiveType: Returns the symbolic value representing the size of this primitive type, i.e., the value of "sizeof(t)".
getSizeofNonPrimitiveTypeFunctionName(SymbolicUniverse) - Static method in class dev.civl.mc.model.IF.ModelConfiguration: Returns the name of the unique function type symbolic constant which maps non-primitive types to their size values.
getSizeofPrimitiveTypeName(SymbolicUniverse, CIVLPrimitiveType.PrimitiveTypeKind) - Static method in class dev.civl.mc.model.IF.ModelConfiguration: Returns the name of the unique symbolic constant which represents the value of the size of a specific CIVLPrimitiveType.
getSoleOutgoing() - Method in interface dev.civl.mc.model.IF.location.Location: Returns the sole outgoing statement from this location.
getSource() - Method in exception class dev.civl.mc.model.IF.CIVLException
getSource() - Method in interface dev.civl.mc.model.IF.Sourceable
getStackEntries() - Method in interface dev.civl.mc.state.IF.ProcessState: Returns an iterable object over the entries in this stack.
getStateVariable() - Method in interface dev.civl.mc.model.IF.type.CIVLType: If a type is defined using a struct, union, or typedef, and it contains state, it may have to be evaluated and stored in a variable of type CIVLDynamicType.
getStaticElementType() - Method in interface dev.civl.mc.model.IF.statement.MallocStatement: Returns the static type of the elements that are to be allocated.
getStaticElementType(int) - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
getStaticTypeOfDynamicType(SymbolicExpression) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Given a symbolic expression returned by the method CIVLTypeFactory.expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), this returns the CIVLType which is associated to the dynamic type that was used to create the given expression.
getStep() - Method in interface dev.civl.mc.model.IF.expression.RegularRangeExpression: Returns the step argument step if it is present, else returns null
getStepOfRegularRange(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the step of the given range Precondition: range is a regular range
getString(CIVLSource, State, int, String, Expression, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Evaluator: extracts a string based on a given character pointer or string literal.
getStringExpression(State, int, String, CIVLSource, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Given a pointer to char, returns the symbolic expression of type array of char which is the string pointed to.
getSubArray(State, int, SymbolicExpression, NumericExpression, NumericExpression, CIVLSource) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: 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.
getSummary(boolean) - Method in interface dev.civl.mc.model.IF.CIVLSource: Returns summary of location and text.
getSymRef(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Given a pointer value, returns the symbolic reference component of that value.
getTransition() - Method in interface dev.civl.mc.kripke.IF.AtomicStep: Returns the transition associated to this atomic step.
getTrueBranch() - Method in interface dev.civl.mc.model.IF.expression.ConditionalExpression
getType() - Method in interface dev.civl.mc.model.IF.expression.DynamicTypeOfExpression
getType(SymbolicExpression) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Given a symbolic expression returned by the method CIVLTypeFactory.expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), this extracts the type that was used to create that expression.
getTypeArgument() - Method in interface dev.civl.mc.model.IF.expression.SizeofTypeExpression: Returns the CIVL type, which is the sole argument of the sizeof operator.
getTypeForOffset() - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression
getUndefinedValue() - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
getUniverse() - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Gets the symbolic universe used by this symbolic analyzer.
getUnreportedViolatedPredicate() - Method in interface dev.civl.mc.predicate.IF.AndPredicate: Returns that predicate that has a violation that not yet been reported.
getUnreportedViolation() - Method in interface dev.civl.mc.predicate.IF.CIVLStatePredicate: Returns the violation that has not yet been reported.
getValue(int) - Method in interface dev.civl.mc.state.IF.DynamicScope: Gets the value of the variable with variable ID vid.
getValues() - Method in interface dev.civl.mc.state.IF.DynamicScope: Returns an iterable object over the variable values.
getValueSetUtility() - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility
getVariableId(CIVLSource, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Given a pointer value, returns the variable ID component of that value.
getVariables() - Method in interface dev.civl.mc.model.IF.statement.AtomicLockAssignStatement: Returns the set of all external variables that could be accessed in an execution of an atomic block.
getVariableValue(int, int) - Method in interface dev.civl.mc.state.IF.State: Given a dyscope ID and a variable ID, returns the value of the first corresponding variable.
getVid(Variable) - Method in interface dev.civl.mc.model.IF.Scope
getViolation() - Method in interface dev.civl.mc.predicate.IF.CIVLStatePredicate
getVSReferenceToSequenceOrNoop(CIVLType, boolean, ValueSetReference) - Method in interface dev.civl.mc.dynamic.IF.ValueSetUtility: This method over-approximates vsRef if it references into sequence elements.
getWaitsforList() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Get an iterable collection of expressions which contains arguments of a "waitsfor" clause.
GNUC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
GOTO - Enum constant in enum class dev.civl.mc.model.IF.statement.NoopStatement.NoopKind
gotoBranchStatement(CIVLSource, Location, String) - Method in interface dev.civl.mc.model.IF.ModelFactory: A goto branch statement is of the form goto label; .
GREEN - Enum constant in enum class dev.civl.mc.util.IF.Utils.Color
guard() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: Returns the guard of the function.
guard() - Method in interface dev.civl.mc.model.IF.statement.Statement
GUI - Static variable in class dev.civl.mc.config.IF.CIVLConstants
GUIDED - Static variable in class dev.civl.mc.config.IF.CIVLConstants
guidedO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: User guided simulation?

H

hasAssignsClause() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: is there assigns clause in this contract?
hasChild(int) - Method in class dev.civl.mc.util.IF.SeqSet.Node: Does this node have a child with the given index?
hasConstantLength() - Method in interface dev.civl.mc.model.IF.type.CIVLArrayType
hasConstantValue() - Method in interface dev.civl.mc.model.IF.expression.Expression: Checks if this expression has a constant value, i.e., constantValue() != NULL.
hasDependsClause() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: is there depends clause in this contract?
hasDerefs() - Method in interface dev.civl.mc.model.IF.expression.Expression: return true iff the expression has at least one dereferences of a certain pointer variable
hasDerefs() - Method in interface dev.civl.mc.model.IF.location.Location: This location or some location in the future contains dereferences of some pointers.
hasDerefs() - Method in interface dev.civl.mc.model.IF.statement.Statement: return true iff the statement has at least one dereferences
hasEmptyStack() - Method in interface dev.civl.mc.state.IF.ProcessState: Does this process state have an empty call stack?
hasFscanf() - Method in interface dev.civl.mc.model.IF.Model
hasFunctionCalls(AST, List<String>) - Static method in class dev.civl.mc.transform.IF.TransformerFactory
hashCode() - Method in class dev.civl.mc.util.IF.Pair
hashCode() - Method in class dev.civl.mc.util.IF.Triple
hasPointerRef() - Method in interface dev.civl.mc.model.IF.variable.Variable: returns true iff this variable has some pointer reference, e.g., when the variable is pointer type, or an array of pointer, etc.
hasReadsClause() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: is there reads clause in this contract?
hasReferences() - Method in interface dev.civl.mc.model.IF.type.CIVLType: Does this type contain a sub-type of pointer or mem type? A value of such a type may contain references to memory locations and those references can be used to read or modify that memory.
hasRequirementsOrEnsurances() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: is there any requirements or ensurances ?
hasSpawn() - Method in interface dev.civl.mc.model.IF.location.Location: Is a spawn statement reachable from this location?
hasState() - Method in interface dev.civl.mc.model.IF.type.CIVLType: If this type contains any array with non-constant extent, it "has state" in the sense that the dynamic type may depend on the state.
hasStateRefVariables() - Method in interface dev.civl.mc.model.IF.Model: does this model contain any variable that involves state references ($state type)?
hasVariable() - Method in interface dev.civl.mc.model.IF.Scope
hasVariableWtPointer() - Method in interface dev.civl.mc.model.IF.Scope
havoc(State, SymbolicType) - Method in interface dev.civl.mc.semantics.IF.Evaluator: returns an arbitrary symbolic constant with the given type.
HAVOC_PREFIX_INDEX - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The prefix of symbolic constants created by havoc.
HEAP - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
HEAP_OBJECT_PREFIX_INDEX - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The prefix of symbolic constants representing heap objects.
HEAP_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the name of the heap type
HEAP_VAR - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the heap variable of each scope.
HEAP_VARIABLE_INDEX - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The index of the heap variable in the scope.
heapErrorKind() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
heapFieldID() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
heapID() - Method in interface dev.civl.mc.model.IF.type.CIVLMemType.MemoryLocationReference: significant iff CIVLMemType.MemoryLocationReference.isHeapObject()
heapMemUnit(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the heap memory unit involved by the given pointer.
heapObjectID() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
heapSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the symbolic heap type
heapType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the CIVL heap type, which is unique for a given CIVL model.
heapType(String) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns a new, incomplete heap type.
heapValue() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
heapVariableName(Variable) - Static method in interface dev.civl.mc.model.IF.LogicFunction
HERE_OR_ROOT - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
hereOrRootExpression(CIVLSource, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory
HereOrRootExpression - Interface in dev.civl.mc.model.IF.expression
higher() - Method in interface dev.civl.mc.model.IF.expression.ExtendedQuantifiedExpression: returns the higher bound

I

id() - Method in interface dev.civl.mc.model.IF.location.Location
id() - Method in interface dev.civl.mc.model.IF.Scope
ID - Static variable in class dev.civl.mc.config.IF.CIVLConstants
identifier() - Method in interface dev.civl.mc.state.IF.State: The string of the form canonicId:instanceId.
identifier(CIVLSource, String) - Method in interface dev.civl.mc.model.IF.ModelFactory: Get an identifier with the given name.
Identifier - Interface in dev.civl.mc.model.IF: An identifier.
idO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The id of the trace for replay, 0 by default.
IF_ELSE - Enum constant in enum class dev.civl.mc.model.IF.statement.NoopStatement.NoopKind
ifElseBranchStatement(CIVLSource, Location, Expression, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory: An if-else branch statement is introduced to translate if-else statement.
impactMemUnits() - Method in interface dev.civl.mc.model.IF.location.Location: Returns the impact memory unit expressions of this location.
impactScopeOfAtomicOrAtomBlock() - Method in interface dev.civl.mc.model.IF.location.Location: The impact scope of a location is required in the enabler when an atomic/atom block is encountered, in which case the impact scope of all statements in the atomic block should be considered.
IMPLIES - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
inAtomic() - Method in interface dev.civl.mc.state.IF.ProcessState: Check if the current process is in the execution of some atomic block.
incoming() - Method in interface dev.civl.mc.model.IF.location.Location
incompleteArrayType(CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get a new incomplete array type.
incrementAtomicCount() - Method in interface dev.civl.mc.state.IF.ProcessState: Increase the atomic block counter.
index - Variable in class dev.civl.mc.util.IF.SeqSet.Node: The index of this node in the parent's list of children.
index() - Method in interface dev.civl.mc.model.IF.expression.reference.ArraySliceReference: Returns the index expression of the array slice.
index() - Method in interface dev.civl.mc.model.IF.expression.SubscriptExpression
index() - Method in interface dev.civl.mc.model.IF.type.StructOrUnionField
INFER - Enum constant in enum class dev.civl.mc.model.IF.contract.FunctionContract.ContractKind
initBundleType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Initializes the bundle type of the model and return the result.
INITIAL_VALUE - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
initialState(Model) - Method in interface dev.civl.mc.state.IF.StateFactory: Returns the canonic, initial state for a CIVL Model.
initialValueExpression(CIVLSource, Variable) - Method in interface dev.civl.mc.model.IF.ModelFactory: Returns an "initial value" expression for the given variable.
InitialValueExpression - Interface in dev.civl.mc.model.IF.expression: An expression yielding the initial value of a variable.
initialValueOfType(State, int, CIVLType) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Given a CIVLType t, returns the default initial value of an object of t as if the object has static storage.
INPUT - Static variable in class dev.civl.mc.config.IF.CIVLConstants
INPUT_PREIFX_INDEX - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The prefix of symbolic constants representing input variables.
INPUT_WRITE - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
inputO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Specify values of input variables.
inputVariables() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
inputVariables() - Method in interface dev.civl.mc.model.IF.ModelFactory
inputVariablesToStringBuffer(State) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer
inputVariableValueMap(State) - Method in interface dev.civl.mc.state.IF.StateFactory: Returns the map of input variable and their value at the given state; empty map if there are no input variables.
inSubprogram() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
INT - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind
INT - Enum constant in enum class dev.civl.mc.semantics.IF.Format.ConversionType
INT_DIV_NO_CHECKING_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
INT_DIV_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
INT_ITER_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of __int_iter__ type, which is the object type of the handle $int_iter.
INT_OPERATION_TRANSFORMER - Static variable in class dev.civl.mc.config.IF.CIVLConstants
intBit - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Set the upper bound of integers.
INTBIT - Static variable in class dev.civl.mc.config.IF.CIVLConstants
INTEGER - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind
INTEGER_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
integerLiteralExpression(CIVLSource, BigInteger) - Method in interface dev.civl.mc.model.IF.ModelFactory: An integer literal expression.
IntegerLiteralExpression - Interface in dev.civl.mc.model.IF.expression: An integer literal.
integerType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get the integer primitive type.
INTERNAL - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
INTERSECT - Enum constant in enum class dev.civl.mc.model.IF.contract.CompositeEvent.CompositeEventOperator
intersectionWith(SeqSet) - Method in class dev.civl.mc.util.IF.SeqSet
intersects(MemoryUnitSet, MemoryUnitSet) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: This is an over-approximation method of intersection.
intOperationTransformer - Static variable in class dev.civl.mc.config.IF.CIVLConstants: apply int operation transformer? true by default.
IntOperationTransformer - Class in dev.civl.mc.transform.IF: This transformer is used to replace integer division ('/') and integer modulo ('%') in the program with $int_div(int, int) and $int_mod(int, int) functions respectively replace unsigned integer arithmetic operations with corresponding library functions: int $unsigned_add, int $unsigned_subtract, int $unsigned_multiply
IntOperationTransformer(ASTFactory, Map<String, String>, CIVLConfiguration) - Constructor for class dev.civl.mc.transform.IF.IntOperationTransformer
INTTYPES - Static variable in class dev.civl.mc.config.IF.CIVLConstants
INVALID - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: Constant for the name of invalid heap objects.
INVALID_CAST - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
invalidHeapObject(SymbolicType) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Constructs an invalid heap object of a certain type.
inverse(int[]) - Static method in class dev.civl.mc.util.IF.Transmuter: Given a bijection from a subset S of {0,...,n-1} to {0,...,m-1}, returns the inverse of that bijection.
inverse(int[], int) - Static method in class dev.civl.mc.util.IF.Transmuter: Given a bijection from a subset S of {0,...,n-1} to {0,...,m-1}, returns the inverse of that bijection.
IOTransformer - Class in dev.civl.mc.transform.IF: The IO transformer transforms
all function calls printf(...) into frpintf(stdout, ...) all function calls scanf(...) into fscanf(stdin, ...) all function calls fopen(...) into $fopen(...)
IOTransformer(ASTFactory, CIVLConfiguration) - Constructor for class dev.civl.mc.transform.IF.IOTransformer: Creates a new instance of IO transformer.
isAbstractFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction: Is this an abstract function?
isAndPredicate() - Method in interface dev.civl.mc.predicate.IF.CIVLStatePredicate: Is this an And predicate?
isAnonymous() - Method in interface dev.civl.mc.model.IF.type.StructOrUnionField
isArrayType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isArrayTypeallComplete(SymbolicArrayType) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox
isAssignToLeft() - Method in interface dev.civl.mc.model.IF.expression.BinaryExpression: Is the value of this binary expression going to be assigned to the left-hand-side operand?
isAtomicFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction: Is this an atomic function? An atomic function is declared with the specifier $atomic_f.
isBinaryBranching() - Method in interface dev.civl.mc.model.IF.location.Location: if this is a location that contains two outgoing statement and the guards are expr and !expr, repectively.
isBoolType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isBound() - Method in interface dev.civl.mc.model.IF.variable.Variable
isBundleType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isCall() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement: Is this a call (not spawn)?
isCharType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isComplete() - Method in interface dev.civl.mc.model.IF.type.CIVLArrayType
isComplete() - Method in interface dev.civl.mc.model.IF.type.CIVLBundleType
isComplete() - Method in interface dev.civl.mc.model.IF.type.CIVLDomainType
isComplete() - Method in interface dev.civl.mc.model.IF.type.CIVLHeapType
isComplete() - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Is this struct or union type complete?
isConcretePointer(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Tests if the given symbolic expression is a concrete pointer value.
isConcretePointer(SymbolicExpression) - Static method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer
isConst() - Method in interface dev.civl.mc.model.IF.variable.Variable
isContracted() - Method in interface dev.civl.mc.model.IF.CIVLFunction: returns true if and only if the function is contracted.
isContracted() - Method in interface dev.civl.mc.model.IF.statement.LoopBranchStatement: Returns true if and only if this loop is attached with LoopContract
isDefinedPointer(State, SymbolicExpression, CIVLSource) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: 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.
isDerefablePointer(State, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Is this a derefable pointer? In other words, check if the pointer can be dereferenced safely.
isDescendantOf(Scope) - Method in interface dev.civl.mc.model.IF.Scope: Return true if the scope is a descendant of the scope anc
isDescendantOf(State, int, int) - Method in interface dev.civl.mc.state.IF.StateFactory: Checks if one dyscope is strictly the descendant of the other (not equal to).
isDisjointWith(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if the components (either a complete object or a sub-component of an object) that the two pointers point to have no intersection.
isDomainType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isEmpty() - Method in interface dev.civl.mc.model.IF.Fragment: Check if the fragment is empty
isEmpty() - Method in interface dev.civl.mc.state.IF.MemoryUnitSet: returns true iff this memory unit set is empty.
isEmpty() - Method in class dev.civl.mc.util.IF.SeqSet
isEmptyDomain(SymbolicExpression, int, CIVLSource) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns true if and only if the given domain is empty which means there is no elements in the domain.
isEmptyHeap(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if a heap is empty, i.e., either it is the SARL null expression or all heap objects it holds are marked as INVALID (already deallocated).
isEnableMpiContract() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
isEnter() - Method in interface dev.civl.mc.model.IF.statement.LoopBranchStatement: Is this the loop enter or exit statement?
isEntryOfLocalBlock() - Method in interface dev.civl.mc.model.IF.location.Location
isEntryOfUnsafeAtomic() - Method in interface dev.civl.mc.model.IF.location.Location
isEnumerationType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isErrorFree() - Method in interface dev.civl.mc.model.IF.expression.Expression: if this expression is guaranteed to be error-free and thus doesn't need any error checking.
isFair() - Method in class dev.civl.mc.config.IF.CIVLConfiguration: If this is true, and termination is being checked, then a cycle in which some process remains enabled at each state will not be considered a violation of non-termination (as it is not considered to represent a real execution).
isFieldOffset() - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression
isFinalState() - Method in interface dev.civl.mc.state.IF.State: Is this the final state upon execution termination? A state is considered as a final state if it has only one process and the process has empty call stack.
isFreeOfUnsafeloop() - Method in interface dev.civl.mc.model.IF.CIVLFunction
isFunction() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isGuardedLocation() - Method in interface dev.civl.mc.model.IF.location.Location: are the disjunction of the guards of all outgoing statements of this location guarded not TRUE?
isHeapObject() - Method in interface dev.civl.mc.model.IF.type.CIVLMemType.MemoryLocationReference
isHeapType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isHere() - Method in interface dev.civl.mc.model.IF.expression.HereOrRootExpression
isIncompleteArrayType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isInitialization() - Method in interface dev.civl.mc.model.IF.statement.AssignStatement
isInitialized(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if a given value is initialized.
isInitializer() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement
isInLoop() - Method in interface dev.civl.mc.model.IF.location.Location: returns true iff this location has more than one incoming location and is inside a loop.
isInNoopLoop() - Method in interface dev.civl.mc.model.IF.location.Location: Determines if this location lies on a cycle in which every location has exactly one outgoing statement and that outgoing statement is a NoopStatement.
isInput() - Method in interface dev.civl.mc.model.IF.variable.Variable
isInRange(NumericExpression, NumericExpression, NumericExpression, NumericExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Test if the given value is within the range, which is given by an inclusibe lower bound, an exclusibe upper bound and a step
isInRange(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if the given value is within the index-th range of a certain rectangular domain.
isIntegerType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isIntOperationTransiformer() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
isInvalidHeapObject(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Is this heap object invalid?
isJoint(MemoryUnit, MemoryUnit) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: This is an over-approximation method to test if two memory units have any intersection.
isJoint(MemoryUnitSet, MemoryUnit) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: This is an over-approximation method of membership testing.
isJoint(MemoryUnitSet, MemoryUnitSet) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory: This is an over-approximation method to test if two memory unit sets have any intersection.
isLeaf() - Method in class dev.civl.mc.util.IF.SeqSet.Node: Is this node a leaf node? A node is a leaf iff it has 0 children.
isLiteralDomain(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns true if and only if the domain is more precisely a literal domain.
isLogic() - Method in interface dev.civl.mc.model.IF.CIVLFunction
isMallocPointer(CIVLSource, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Is the given pointer the result of some malloc/handle create operation?
isMonitoringReads(int) - Method in interface dev.civl.mc.state.IF.State
isMonitoringWrites(int) - Method in interface dev.civl.mc.state.IF.State
isNondet() - Method in interface dev.civl.mc.model.IF.CIVLFunction
isNormalFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction: Is this a normal function that contains a function body defined in the source code?
isNullPointer(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if a given pointer is a NULL pointer.
isNumericType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
ISO646 - Static variable in class dev.civl.mc.config.IF.CIVLConstants
isOutput() - Method in interface dev.civl.mc.model.IF.variable.Variable
isParameter() - Method in interface dev.civl.mc.model.IF.variable.Variable: Is this variable declared as a parameter of some function?
isPocessIdDefined(int) - Method in interface dev.civl.mc.model.IF.ModelFactory
isPointer2MemoryBlock(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns true iff the given pointer is a pointer to a memory block, where a memory block is defined as a space in heap which is allocated by once execution of $malloc.
isPointerToHeap(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Is the given pointer pointing to a memory space that is part of a heap?
isPointerType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isProcessIdNull(int) - Method in interface dev.civl.mc.model.IF.ModelFactory
isProcessType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isProcNull(SymbolicExpression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Checks if the given process value equals to the $proc_null constant.
isPropertyToggled(CIVLProperty) - Method in class dev.civl.mc.config.IF.CIVLConfiguration: Determines if a toggleable property is toggled, i.e.
isPure() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: Does the contract contains pure clause?
isPureFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction: is this a pure function? i.e., a function that doesn't has side effect in the state
isPurelyLocal() - Method in interface dev.civl.mc.model.IF.CIVLFunction: is this function a purely local function?
isPurelyLocal() - Method in interface dev.civl.mc.model.IF.expression.Expression
isPurelyLocal() - Method in interface dev.civl.mc.model.IF.location.Location
isPurelyLocal() - Method in interface dev.civl.mc.model.IF.statement.Statement
isQuiet() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
isRangeType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isReach() - Method in interface dev.civl.mc.model.IF.contract.MemoryEvent: Is this a \reach event?
isRead() - Method in interface dev.civl.mc.model.IF.contract.MemoryEvent: Is this a \read event?
isRealType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isRectangularDomain(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Is the given domain a rectangular domain?
isRegularRange(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Is the given range a regular range?
isRemovable() - Method in interface dev.civl.mc.model.IF.statement.NoopStatement
isReplay() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
isReported() - Method in exception class dev.civl.mc.log.IF.CIVLExecutionException: Is this error reported?
isReservedFunction() - Method in interface dev.civl.mc.model.IF.LogicFunction
isRoot() - Method in interface dev.civl.mc.model.IF.expression.HereOrRootExpression
isRootFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction
isRun() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement: Pre-condition: CallOrSpawnStatement.isSpawn() == true
isSafeLoop() - Method in interface dev.civl.mc.model.IF.location.Location: Returns true if this loop satisfies the following conditions: has one iteration variable the iteration variable is only modified by the last statement (incremental) the condition has the form i invalid input: '<' N (or i > N) the loop has finite iterations (can be decided statically)
isScalar() - Method in interface dev.civl.mc.model.IF.type.CIVLType: Is this type a scalar type?
isScopeIdDefined(int) - Method in interface dev.civl.mc.state.IF.StateFactory
isScopeType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isSelfDestructable() - Method in interface dev.civl.mc.state.IF.ProcessState
isSetType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isSetTypeOf(CIVLType) - Method in interface dev.civl.mc.model.IF.type.CIVLType
isSleep() - Method in interface dev.civl.mc.model.IF.location.Location: returns true iff this location is the SLEEP location, which has no outgoing statement
isSpawn() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement: Is this a spawn (not call)?
isStart() - Method in interface dev.civl.mc.model.IF.location.Location: Returns true if this location is the start location of a function.
isStateFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction: returns true iff this function is a state function
isStatic() - Method in interface dev.civl.mc.model.IF.variable.Variable: is this variable static qualified?
isStringLiteral() - Method in interface dev.civl.mc.model.IF.expression.CompoundLiteralExpression
isStruct() - Method in interface dev.civl.mc.model.IF.expression.DotExpression
isStructType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isSuperTypeOf(CIVLType) - Method in interface dev.civl.mc.model.IF.type.CIVLType: Is this type the super type of the given sub-type? If subtype is the same as this type, return true.
isSwitchOrChooseWithDefault() - Method in interface dev.civl.mc.model.IF.location.Location: Returns true iff this is a switch or $choose statement location where a set of branch statements emanate from and a default case for it was specified.
isSystemCall() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement: Check if the statement is calling a system function.
isSystemFunction() - Method in interface dev.civl.mc.model.IF.CIVLFunction: Is this a system function? A system function doesn't contain a function body and it is implemented by a library component in Java.
isSystemSource() - Method in interface dev.civl.mc.model.IF.CIVLSource: Checks if this source is some system source not from input program.
isTemporary() - Method in interface dev.civl.mc.model.IF.statement.NoopStatement: is this a temporary noop that is inserted by the model builder and should be removed from the model?
isToggleableProperty(CIVLProperty) - Method in class dev.civl.mc.config.IF.CIVLConfiguration: Determines whether a CIVLProperty is toggleable.
isTrue(Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Check if a certain expression is TRUE.
isUnion() - Method in interface dev.civl.mc.model.IF.expression.DotExpression
isUnionType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isValidRefOf(ReferenceExpression, SymbolicType) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Checks if the given reference is valid for the symbolic type of a certain object value.
isVariableDeclaration() - Method in interface dev.civl.mc.model.IF.statement.NoopStatement: is this noop associating to a variable declaration?
isVoidType() - Method in interface dev.civl.mc.model.IF.type.CIVLType
isWrite() - Method in interface dev.civl.mc.model.IF.contract.MemoryEvent: Is this a \write event?
iterator() - Method in class dev.civl.mc.util.IF.SeqSet.Node: Returns a new iterator over childrenIndexes.
iterator() - Method in class dev.civl.mc.util.IF.Singleton

K

Kripkes - Class in dev.civl.mc.kripke.IF: This is the entry point of the module kripke.
Kripkes() - Constructor for class dev.civl.mc.kripke.IF.Kripkes

L

LAMBDA - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

lambdaExpression(CIVLSource, CIVLFunctionType, Variable, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Creates a new lambda expression.

LambdaExpression - Interface in dev.civl.mc.model.IF.expression

A CIVL-C quanti, bound variable declaration list, (optional) restriction and expression.

lambdaFunction() - Method in interface dev.civl.mc.model.IF.expression.LambdaExpression

The expression e(x).

LDOUBLE_COMPLEX_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

The CIVL-C struct type corresponding to C's long double _Complex.

leafNodeReferencesOfType(CIVLSource, State, int, CIVLType) - Method in interface dev.civl.mc.semantics.IF.Evaluator

leastCommonAncestor(Scope, Scope) - Method in interface dev.civl.mc.model.IF.ModelFactory

leaveAtomic() - Method in interface dev.civl.mc.model.IF.location.Location

leaveAtomic() - Method in interface dev.civl.mc.model.IF.statement.AtomicLockAssignStatement

leaveAtomic(State, int) - Method in interface dev.civl.mc.state.IF.StateFactory

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.

left - Variable in class dev.civl.mc.util.IF.Pair

left() - Method in interface dev.civl.mc.model.IF.contract.CompositeEvent

Returns the left operand.

left() - Method in interface dev.civl.mc.model.IF.expression.BinaryExpression

LESS_THAN - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR

LESS_THAN_EQUAL - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR

lexicalScope() - Method in interface dev.civl.mc.state.IF.DynamicScope

Returns the lexical (static) scope of which this dynamic scope is an instance.

lhs() - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

LHSExpression - Interface in dev.civl.mc.model.IF.expression

A left-hand-side expression.

LHSExpression.LHSExpressionKind - Enum Class in dev.civl.mc.model.IF.expression

lhsExpressionKind() - Method in interface dev.civl.mc.model.IF.expression.LHSExpression

library() - Method in interface dev.civl.mc.model.IF.expression.SystemGuardExpression

The name of the library that the invoked function belongs to.

LIBRARY - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty

LIBRARY_PREFIX - Static variable in class dev.civl.mc.config.IF.CIVLConstants

The prefix of the full name of the class of a library enabler/executor.

LibraryEnabler - Interface in dev.civl.mc.kripke.IF

A Library Enabler provides a method to compute the enabled transitions of system function calls at a certain state for a give process.

LibraryEnablerLoader - Interface in dev.civl.mc.kripke.IF

The library enabler loader provides the mechanism for loading the library enabler of a certain library.

LibraryEvaluator - Interface in dev.civl.mc.semantics.IF

A Library Evaluator provides a method to "evaluate" the guard of each system function call.

LibraryEvaluatorLoader - Interface in dev.civl.mc.semantics.IF

The library evaluator loader provides the mechanism for loading the library evaluator of a certain library.

LibraryExecutor - Interface in dev.civl.mc.semantics.IF

A Library Executor provides the semantics for system functions defined in a library.

LibraryExecutorLoader - Interface in dev.civl.mc.semantics.IF

The library executor loader provides the mechanism for loading the library executor of a certain library.

LibraryLoaderException - Exception Class in dev.civl.mc.semantics.IF

A library loader exception is produced by errors occur during when a library executor/evaluator/enabler loader attempts to load a specific library executor/evaluator/enabler.

LibraryLoaderException(String) - Constructor for exception class dev.civl.mc.semantics.IF.LibraryLoaderException

Creates a new instance of library loader exception.

LIMITS - Static variable in class dev.civl.mc.config.IF.CIVLConstants

LINEAR_ORDER - Enum constant in enum class dev.civl.mc.model.IF.AbstractFunction.SpecialRelationKind

this abstract function represents a linear order binary relation

LINK - Static variable in class dev.civl.mc.config.IF.CIVLConstants

linkO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Link a source file with the target program.

literalDomainSearcher(SymbolicExpression, List<SymbolicExpression>, int) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Iterating a literal domain to match a given domain element.

LiteralExpression - Interface in dev.civl.mc.model.IF.expression

The parent of all literal expressions.

LiteralExpression.LiteralKind - Enum Class in dev.civl.mc.model.IF.expression

literalKind() - Method in interface dev.civl.mc.model.IF.expression.LiteralExpression

LOC - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.ErrorStateEquivalence

LOCALE - Static variable in class dev.civl.mc.config.IF.CIVLConstants

location() - Method in interface dev.civl.mc.state.IF.StackEntry

Returns the static location component of this activation frame.

location(CIVLSource, Scope) - Method in interface dev.civl.mc.model.IF.ModelFactory

Create a new location.

Location - Interface in dev.civl.mc.model.IF.location

The parent of all locations.

Location.AtomicKind - Enum Class in dev.civl.mc.model.IF.location

Atomic flags of a location: NONE: no $atomic boundary; ATOMIC_ENTER/ATOM_ENTER: the location is the starting point of an $atomic block; ATOMIC_EXIT/ATOM_EXIT: the location is the ending point of an $atomic block.

locations() - Method in interface dev.civl.mc.model.IF.CIVLFunction

locationStepString() - Method in interface dev.civl.mc.model.IF.statement.Statement

Get the string representation in the form of: source location id -> target location id e.g.

lockedByAtomic(State) - Method in interface dev.civl.mc.state.IF.StateFactory

Checks if any process at the state is holding the atomic lock, i.e, the process is executing some atomic blocks.

logError(CIVLSource, State, int, StringBuffer, BooleanExpression, ValidityResult.ResultType, CIVLProperty, String) - Method in class dev.civl.mc.log.IF.CIVLErrorLogger

Report a (possible) error detected in the course of evaluating an expression.

logicFunction(CIVLSource, Identifier, Scope, List<Variable>, CIVLType, int[], Scope, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Create a new logic function (LogicFunction).

LogicFunction - Interface in dev.civl.mc.model.IF

A logic function is a function whose definition (body) is either absent (i.e.

logSimpleError(CIVLSource, State, int, String, StringBuffer, CIVLProperty, String) - Method in class dev.civl.mc.log.IF.CIVLErrorLogger

Checks whether the path condition is satisfiable and logs an error if it is (or might be).

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.AnnotationTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.ComplexTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.ContractTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.Cuda2CIVLTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.GeneralTransformer

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.IntOperationTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.IOTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.LoopContractTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.MPI2CIVLTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.OpenMP2CIVLTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.OpenMPSimplifier

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.Pthread2CIVLTransformer

The long name of the transformer.

LONG_NAME - Static variable in class dev.civl.mc.transform.IF.ShortCircuitTransformer

LOOP - Enum constant in enum class dev.civl.mc.model.IF.contract.FunctionContract.ContractKind

LOOP - Enum constant in enum class dev.civl.mc.model.IF.statement.NoopStatement.NoopKind

LOOP_ASSIGNS_GEN - Static variable in class dev.civl.mc.config.IF.CIVLConstants

LOOP_ASSIGNS_GEN_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants

LOOP_INV - Static variable in class dev.civl.mc.config.IF.CIVLConstants

loopAnalysis() - Method in interface dev.civl.mc.model.IF.location.Location

Determines whether this location lies on a cycle in which every location has exactly one outgoing statement and that outgoing statement is a NoopStatement, then calls

invalid reference

#setInNoopLoop(boolean)

with appropriate boolean value.

loopAssigns() - Method in interface dev.civl.mc.model.IF.contract.LoopContract

Returns an array of loop assigns specified for this loop.

loopBranchStatement(CIVLSource, Location, Expression, boolean, LoopContract) - Method in interface dev.civl.mc.model.IF.ModelFactory

An loop branch statement is introduced when translating a loop.

LoopBranchStatement - Interface in dev.civl.mc.model.IF.statement

loopContract(CIVLSource, Location, List<Expression>, List<LHSExpression>, List<Expression>) - Method in interface dev.civl.mc.model.IF.ModelFactory

Creates a LoopContract instance

LoopContract - Interface in dev.civl.mc.model.IF.contract

This class represents a group of loop annotations for a loop, including loop invariants, loop assigns and loop variants.

LoopContractTransformer - Class in dev.civl.mc.transform.IF

LoopContractTransformer(ASTFactory, CIVLConfiguration) - Constructor for class dev.civl.mc.transform.IF.LoopContractTransformer

loopInvariantEnabled() - Method in class dev.civl.mc.config.IF.CIVLConfiguration

loopInvariants() - Method in interface dev.civl.mc.model.IF.contract.LoopContract

Returns an array of loop invariants specified for this loop.

loopLocation() - Method in interface dev.civl.mc.model.IF.contract.LoopContract

Returns the location which identifies the corresponding loop.

loopO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Enable all settings that are required for verifying with loop invariants.

loopVariables() - Method in interface dev.civl.mc.model.IF.statement.DomainIteratorStatement

Returns the list of loop variables, ordered from left to right.

loopVariants() - Method in interface dev.civl.mc.model.IF.contract.LoopContract

Returns an array of loop variants specified for this loop.

lower() - Method in interface dev.civl.mc.model.IF.expression.ExtendedQuantifiedExpression

returns the lower bound

lowerBounds() - Method in interface dev.civl.mc.model.IF.expression.DifferentiableExpression

Gets the lower bounds of the intervals.

lowestCommonAncestor(State, int, int) - Method in interface dev.civl.mc.state.IF.StateFactory

Computes the lowest common ancestor of two given dyscopes.

lowestScope() - Method in interface dev.civl.mc.model.IF.expression.Expression

lowestScope() - Method in interface dev.civl.mc.model.IF.statement.Statement

Obtains the lowest scope of expression accessed by this statement.

M

MACRO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
macroO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Define macros.
main(String[]) - Static method in class dev.civl.mc.CIVL: Execute the appropriate CIVL tool(s) based on the command line arguments.
makeArrayElementReference(ReferenceExpression, NumericExpression[]) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns an array element reference by giving the array reference and the coordinates to indexing the element.
makeFull() - Method in class dev.civl.mc.util.IF.SeqSet: Makes this the full set (consisting of all tuples).
makeFunctionPointer(int, int) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility
makePointer(int, int, ReferenceExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Makes a pointer value from the given dynamic scope ID, variable ID, and symbolic reference value.
makePointer(SymbolicExpression, ReferenceExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Constructs a new pointer by replacing the reference expression of a given pointer.
malloc(CIVLSource, State, int, String, Expression, SymbolicExpression, CIVLType, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Executor: Adds a new object to the heap of a certain scope; returns the pointer of the object in the heap.
malloc(State, int, int, int, SymbolicType, NumericExpression) - Method in interface dev.civl.mc.state.IF.StateFactory: Allocates an object for the given malloc ID in the heap of the given dyscope.
malloc(State, int, int, SymbolicExpression) - Method in interface dev.civl.mc.state.IF.StateFactory: Allocates an object, of the given value, for the given malloc ID in the heap of the given dyscope.
MALLOC - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
MALLOC - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind: Memory allocation
mallocID() - Method in interface dev.civl.mc.model.IF.type.CIVLMemType.MemoryLocationReference: significant iff CIVLMemType.MemoryLocationReference.isHeapObject()
mallocStatement(CIVLSource, Location, LHSExpression, CIVLType, Expression, Expression, int, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Create a new malloc statement
MallocStatement - Interface in dev.civl.mc.model.IF.statement: A statement for dynamic allocation of objects.
MATH - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MATH_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MAX_DEPTH - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MAX_PROCS - Static variable in class dev.civl.mc.config.IF.CIVLConstants
maxdepthO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The maximal depth for search.
maxProcs() - Method in class dev.civl.mc.kripke.IF.CIVLStateManager
maxProcsO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MAYBE - Enum constant in enum class dev.civl.mc.model.IF.CIVLException.Certainty: The prover is not sure whether this is an error.
mdArrayRead(SymbolicExpression, NumericExpression[]) - Method in interface dev.civl.mc.semantics.IF.ArrayCutter: Read a multi-dimensional array
mdArrayRead(SymbolicExpression, NumericExpression[]) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox: Read a multi-dimensional array
mdArrayWrite(SymbolicExpression, NumericExpression[], SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.ArrayCutter: Write a value to a multi-dimensional array
mdArrayWrite(SymbolicExpression, NumericExpression[], SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox: Write a value to a multi-dimensional array
MEM - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind: the type represents a set of pointers, see CIVLMemType
MEM - Static variable in class dev.civl.mc.config.IF.CIVLConstants
memEqO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
memEvaluator() - Method in interface dev.civl.mc.semantics.IF.Evaluator
MEMORY_LEAK - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
MEMORY_MANAGE - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
MEMORY_UNIT - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
MemoryEvent - Interface in dev.civl.mc.model.IF.contract: This represents a \read or \write event of a depends clause.
MemoryUnit - Interface in dev.civl.mc.state.IF: A memory unit represents an object or a part of an object that can be accessed through an expression, e.g., a[9].x, b[8], c, etc.
memoryUnitEvaluator() - Method in interface dev.civl.mc.semantics.IF.Evaluator
memoryUnitExpression(CIVLSource, Variable, CIVLType, MemoryUnitReference, boolean, boolean) - Method in interface dev.civl.mc.model.IF.ModelFactory: creates a memory unit expression.
MemoryUnitExpression - Interface in dev.civl.mc.model.IF.expression: A memory unit expression is an expression that represents (part of) the memory related to some variable.
MemoryUnitExpressionEvaluator - Interface in dev.civl.mc.semantics.IF
MemoryUnitFactory - Interface in dev.civl.mc.state.IF
memoryUnitKind() - Method in interface dev.civl.mc.model.IF.expression.reference.MemoryUnitReference: The reference kind of this memory unit.
MemoryUnitReference - Interface in dev.civl.mc.model.IF.expression.reference
MemoryUnitReference.MemoryUnitReferenceKind - Enum Class in dev.civl.mc.model.IF.expression.reference
memoryUnits() - Method in interface dev.civl.mc.model.IF.contract.MemoryEvent: Returns the memory units associated with this event.
memoryUnits() - Method in interface dev.civl.mc.state.IF.MemoryUnitSet: Gets the memory units of this set.
MemoryUnitSet - Interface in dev.civl.mc.state.IF: A memory unit set represents a set of memory units.
memoryUnitToString(State, MemoryUnit) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Pretty representation of a memory unit.
memUnitFactory() - Method in interface dev.civl.mc.state.IF.StateFactory: returns the memory unit factory associated with this state factory, which contains utility functions for
memValueCollector(SymbolicUniverse, SymbolicExpression) - Method in interface dev.civl.mc.model.IF.type.CIVLMemType: Returns a UnaryOperator to $mem values that will clean up references in the $mem value.
memValueCreator(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLMemType
memValueIterator() - Method in interface dev.civl.mc.model.IF.type.CIVLMemType
mesageType() - Method in interface dev.civl.mc.model.IF.Model
message - Variable in exception class dev.civl.mc.state.IF.CIVLStateException
message() - Method in exception class dev.civl.mc.state.IF.CIVLHeapException
message() - Method in exception class dev.civl.mc.state.IF.CIVLStateException
MESSAGE_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the name of message type
MIN - Static variable in class dev.civl.mc.config.IF.CIVLConstants
minO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Search for the minimum counterexample? false by default.
MINUS - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
model() - Method in interface dev.civl.mc.model.IF.CIVLFunction
model() - Method in interface dev.civl.mc.model.IF.ModelFactory: Returns the CIVL model built by this model factory.
model() - Method in interface dev.civl.mc.model.IF.Scope
model() - Method in interface dev.civl.mc.model.IF.statement.Statement
model(CIVLSource, CIVLFunction, Program) - Method in interface dev.civl.mc.model.IF.ModelFactory: Create a new model.
Model - Interface in dev.civl.mc.model.IF: A model of a CIVL program.
ModelBuilder - Interface in dev.civl.mc.model.IF: Class to provide translation from an AST to a model.
ModelConfiguration - Class in dev.civl.mc.model.IF: This file contains the constants used by the model builder/translator, which reflects the translation strategy of CIVL.
ModelConfiguration() - Constructor for class dev.civl.mc.model.IF.ModelConfiguration
modelFactory() - Method in interface dev.civl.mc.semantics.IF.Evaluator: The model factory should be the unique one used in the system.
ModelFactory - Interface in dev.civl.mc.model.IF: The factory to create all model components.
Models - Class in dev.civl.mc.model.IF: This is the entry point of the module model.
Models() - Constructor for class dev.civl.mc.model.IF.Models
MODULO - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
MPI - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MPI_CONTRACT - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MPI_DEFS - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MPI_DEFS_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MPI_ERROR - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
MPI_MODEL - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MPI_NPROCS_MAX - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The maximum number of MPI processes a user can request.
MPI_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
MPI_SYS_STATUS - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the variable representing the status of an MPI process, which is modified by MPI_Init() and MPI_Finalized().
MPI2CIVLTransformer - Class in dev.civl.mc.transform.IF: MPI2CIVLTransformer transforms an AST of an MPI program into an AST of an equivalent CIVL-C program.
MPI2CIVLTransformer(ASTFactory) - Constructor for class dev.civl.mc.transform.IF.MPI2CIVLTransformer: Creates a new instance of MPITransformer.
mpiContractFunction() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
mpiContractO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: MPI contract mode? Disable by default.
mpiModel() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
mpiModelO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Chooses MPI implementation models (see CIVLConstants.MPIModelKind).
myMathPower(int, int) - Static method in class dev.civl.mc.util.IF.Utils
myPower(int, int) - Static method in class dev.civl.mc.util.IF.Utils

N

name() - Method in interface dev.civl.mc.model.IF.CIVLFunction
name() - Method in interface dev.civl.mc.model.IF.contract.NamedFunctionBehavior: Returns the name of this behavior.
name() - Method in interface dev.civl.mc.model.IF.expression.BoundVariableExpression
name() - Method in interface dev.civl.mc.model.IF.Identifier
name() - Method in interface dev.civl.mc.model.IF.Model
name() - Method in interface dev.civl.mc.model.IF.type.CIVLEnumType: Gets the name of the enumeration type.
name() - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Returns the name of this struct or union type.
name() - Method in interface dev.civl.mc.model.IF.type.StructOrUnionField
name() - Method in interface dev.civl.mc.model.IF.variable.Variable
name() - Method in interface dev.civl.mc.state.IF.ProcessState: This name is not part of the state.
namedBehaviors() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: Returns the named behaviors of the function.
NamedFunctionBehavior - Interface in dev.civl.mc.model.IF.contract: A named behavior contains a name and assumptions in addition to those components contained by FunctionBehavior.
needsEnabler() - Method in interface dev.civl.mc.model.IF.SystemFunction: returns true iff this system function needs special handling from the library enabler.
NEGATIVE - Enum constant in enum class dev.civl.mc.model.IF.expression.UnaryExpression.UNARY_OPERATOR
newAndPredicate(CIVLStatePredicate) - Static method in class dev.civl.mc.predicate.IF.Predicates
newAnonymousVariable(CIVLSource, Scope, CIVLType) - Method in interface dev.civl.mc.model.IF.ModelFactory: Create a variable of the given type and add it to the given scope.
newAnonymousVariableForArrayLiteral(CIVLSource, Scope, CIVLArrayType) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates an anonymous variable of array type in a certain scope.
newAnonymousVariableForConstantArrayLiteral(CIVLSource, CIVLArrayType, SymbolicExpression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates an anonymous variable of array type in the static constant scope.
newAnyactEvent(CIVLSource) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new instance of \anyact event
newArray(BooleanExpression, SymbolicType, NumericExpression, SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Creates a new array of given length, using the given type as its element type, and each element having the given value.
newArrayShape(SymbolicArrayType) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox: create an ArrayToolBox.ArrayShape, the base type will be (default) non-array type
newArrayShape(SymbolicArrayType, SymbolicType) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox: create an ArrayToolBox.ArrayShape with a specified base type.
newArraySlice(SymbolicExpression, NumericExpression[], NumericExpression, SymbolicType) - Method in interface dev.civl.mc.semantics.IF.ArrayToolBox: create an ArrayToolBox.ArraySlice.
newArrayToolBox(SymbolicUniverse) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Return a new ArrayToolBox
newCallEvent(CIVLSource, CIVLFunction, List<Expression>) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new instance of call event.
newCompositeEvent(CIVLSource, CompositeEvent.CompositeEventOperator, DependsEvent, DependsEvent) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new instance of composite event.
newDeadlock(SymbolicUniverse, Enabler, StateFactory, SymbolicAnalyzer) - Static method in class dev.civl.mc.predicate.IF.Predicates
newDependencyAnalyzer(StateManager<State, Transition>, StateFactory, SimpleEnabler) - Static method in class dev.civl.mc.kripke.IF.Kripkes
newDynamicMemoryLocationSetFactory(SymbolicUniverse, CIVLTypeFactory, SymbolicExpression) - Static method in class dev.civl.mc.dynamic.IF.Dynamics: Creates a new instance of DynamicMemoryLocationSetFactory.
newEnabler(StateFactory, Evaluator, Executor, SymbolicAnalyzer, MemoryUnitFactory, LibraryEnablerLoader, CIVLErrorLogger, CIVLConfiguration, GMCConfiguration) - Static method in class dev.civl.mc.kripke.IF.Kripkes: Creates a new instance of enabler.
newErrorSideEffectFreeEvaluator(ModelFactory, StateFactory, LibraryEvaluatorLoader, LibraryExecutorLoader, SymbolicUtility, SymbolicAnalyzer, MemoryUnitFactory, CIVLErrorLogger, CIVLConfiguration) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new instance of ErrorSideEffectFreeEvaluator.
newEvaluator(ModelFactory, StateFactory, LibraryEvaluatorLoader, LibraryExecutorLoader, SymbolicUtility, SymbolicAnalyzer, MemoryUnitFactory, CIVLErrorLogger, CIVLConfiguration) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new instance of CIVL evaluator.
newExecutor(ModelFactory, StateFactory, LibraryExecutorLoader, Evaluator, SymbolicAnalyzer, CIVLErrorLogger, CIVLConfiguration) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new instance of CIVL executor.
newFunctionalEquivalence(SymbolicUniverse, SymbolicAnalyzer, String[], Map<BooleanExpression, Set<Pair<State, SymbolicExpression[]>>>) - Static method in class dev.civl.mc.predicate.IF.Predicates
newFunctionBehavior(CIVLSource) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new function behavior.
newFunctionContract(CIVLSource, Scope) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new function contract.
newImmutableMemoryUnitFactory(SymbolicUniverse) - Static method in class dev.civl.mc.state.IF.States
newImmutableStateFactory(ModelFactory, MemoryUnitFactory, CIVLConfiguration) - Static method in class dev.civl.mc.state.IF.States: Returns a new immutable state factory based on the given model factory.
newLibraryEnablerLoader(LibraryEvaluatorLoader, CIVLConfiguration) - Static method in class dev.civl.mc.kripke.IF.Kripkes: Creates a new instance of library enabler loader.
newLibraryEvaluatorLoader(CIVLConfiguration) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new instance of library evaluator loader.
newLibraryExecutorLoader(LibraryEvaluatorLoader, CIVLConfiguration) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new instance of library executor loader.
newMemoryEvent(CIVLSource, DependsEvent.DependsEventKind, Set<Expression>) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new instance of memory event of the given kind.
newMemoryUnit(int, int, ReferenceExpression) - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory
newMemoryUnitEvaluator(Evaluator, MemoryUnitFactory) - Static method in class dev.civl.mc.semantics.IF.Semantics
newMemoryUnitSet() - Method in interface dev.civl.mc.state.IF.MemoryUnitFactory
newModelBuilder(ModelFactory) - Static method in class dev.civl.mc.model.IF.Models: Creates a new instance of model builder.
newModelBuilder(SymbolicUniverse, CIVLConfiguration) - Static method in class dev.civl.mc.model.IF.Models: Creates a new instance of model builder.
newNamedFunctionBehavior(CIVLSource, String) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new named function behavior
newNoactEvent(CIVLSource) - Method in interface dev.civl.mc.model.IF.contract.ContractFactory: Creates a new instance of \noact event
newNoopTransition(int, BooleanExpression, Statement, boolean) - Static method in class dev.civl.mc.semantics.IF.Semantics: Create a new NoopTransition whose statement will not be executed.
newPotentialDeadlock(SymbolicUniverse, Enabler, LibraryEnablerLoader, Evaluator, ModelFactory, SymbolicUtility, SymbolicAnalyzer) - Static method in class dev.civl.mc.predicate.IF.Predicates
newReadSetCollectEvaluator() - Method in interface dev.civl.mc.semantics.IF.Evaluator
newStateManager(Enabler, Executor, SymbolicAnalyzer, CIVLErrorLogger, CIVLConfiguration) - Static method in class dev.civl.mc.kripke.IF.Kripkes: Creates a new instance of state manager.
newSymbolicAnalyzer(CIVLConfiguration, CIVLErrorLogger, SymbolicUniverse, ModelFactory, SymbolicUtility) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new instance of symbolic analyzer.
newSymbolicUtility(SymbolicUniverse, ModelFactory, StateFactory) - Static method in class dev.civl.mc.dynamic.IF.Dynamics: Creates a new instance of symbolic utility.
newTransformerFactory(ASTFactory) - Static method in class dev.civl.mc.transform.IF.Transforms
newTransition(int, BooleanExpression, Statement) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new regular Transition whose statement will be executed by executor.
newTransition(int, BooleanExpression, Statement, boolean) - Static method in class dev.civl.mc.semantics.IF.Semantics: Creates a new regular Transition whose statement will be executed by executor.
newTrivialPredicate() - Static method in class dev.civl.mc.predicate.IF.Predicates
NEXT_TIME_COUNT - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the function to get the unique counter of time
NOACT - Enum constant in enum class dev.civl.mc.model.IF.contract.DependsEvent.DependsEventKind
Node(SeqSet.Node, int) - Constructor for class dev.civl.mc.util.IF.SeqSet.Node: Creates new node with given index, empty set of childrenIndexes.
NON_BLOCKING - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.MPIModelKind
nondetFunction(CIVLSource, Identifier, CIVLType, Scope) - Method in interface dev.civl.mc.model.IF.ModelFactory
NONE - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.DeadlockKind
NONE - Enum constant in enum class dev.civl.mc.model.IF.AbstractFunction.SpecialRelationKind: this abstract function is not representing a special relation
NONE - Enum constant in enum class dev.civl.mc.model.IF.CIVLException.Certainty: Probably an internal CIVL error: the theorem prover hasn't said anything.
NONE - Enum constant in enum class dev.civl.mc.model.IF.location.Location.AtomicKind
NONE - Enum constant in enum class dev.civl.mc.model.IF.statement.NoopStatement.NoopKind
NONEMPTY - Enum constant in enum class dev.civl.mc.state.IF.CIVLHeapException.HeapErrorKind
NOOP - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind: No operation
NOOP - Enum constant in enum class dev.civl.mc.semantics.IF.Transition.TransitionKind
noopKind() - Method in interface dev.civl.mc.model.IF.statement.NoopStatement: Returns the kind of this noop statement, which might be a if-else branching, loop branching, atomic entering/exiting noop statement, etc.
noopStatement(CIVLSource, Location, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: A noop statement with the default guard of true.
NoopStatement - Interface in dev.civl.mc.model.IF.statement: Marker interface for a noop statement.
NoopStatement.NoopKind - Enum Class in dev.civl.mc.model.IF.statement
noopStatementForVariableDeclaration(CIVLSource, Location) - Method in interface dev.civl.mc.model.IF.ModelFactory: A temporary noop statement with the true guard
noopStatementTemporary(CIVLSource, Location) - Method in interface dev.civl.mc.model.IF.ModelFactory: A temporary noop statement with the true guard
noopStatementWtGuard(CIVLSource, Location, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: A noop statement with an explicit guard expression.
NORMAL - Enum constant in enum class dev.civl.mc.semantics.IF.Transition.TransitionKind
NOT - Enum constant in enum class dev.civl.mc.model.IF.expression.UnaryExpression.UNARY_OPERATOR
NOT_EQUAL - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
nothing(CIVLSource) - Method in interface dev.civl.mc.model.IF.ModelFactory
Nothing - Interface in dev.civl.mc.model.IF.expression
NOTHING - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
NPROCS - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the input variable denoting the number of MPI processes in the final CIVL-C program.
NPROCS_LOWER_BOUND - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the input variable denoting the lower bound of the number of MPI processes in the final CIVL-C program.
NPROCS_UPPER_BOUND - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the input variable denoting the upper bound of the number of MPI processes in the final CIVL-C program.
NULL_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
NULL_POINTER_DYSCOPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
NULL_POINTER_VID - Static variable in class dev.civl.mc.model.IF.ModelConfiguration
nullFunctionPointer() - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility
nullPointer() - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Returns the NULL pointer of CIVL.
nullPointerExpression(CIVLPointerType, CIVLSource) - Method in interface dev.civl.mc.model.IF.ModelFactory: Generate a null pointer expression
nullProcessValue() - Method in interface dev.civl.mc.model.IF.ModelFactory
nullScopeValue() - Method in interface dev.civl.mc.state.IF.StateFactory
numArguments() - Method in interface dev.civl.mc.model.IF.contract.CallEvent: Returns the number of arguments of the call event.
numAssignsMemoryUnits() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the number of assigns clauses of this behavior.
numberOfReachers(int) - Method in interface dev.civl.mc.state.IF.State: How many processes can reach this dynamic scope? A process p can reach a dynamic scope d iff there is a path starting from a dynamic scope which is referenced in a frame on p's call stack to d, following the "parent" edges in the scope tree.
numberOfValues() - Method in interface dev.civl.mc.state.IF.DynamicScope: Returns the number of variable values stored in the dynamic scope.
numBoundVariables() - Method in interface dev.civl.mc.model.IF.expression.QuantifiedExpression
numDependsEvents() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the number of depends events of this behavior.
numDyscopes() - Method in interface dev.civl.mc.state.IF.State: Returns the number of dynamic scopes in this state.
numEnsurances() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the number of postconditions of this behavior.
numericExpression(Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Translates an expression to be of numeric-type (i.e., int or real).
numFields() - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType: Returns the number of fields in this struct or union type.
numFunctions() - Method in interface dev.civl.mc.model.IF.Scope
numLiveProcs() - Method in interface dev.civl.mc.state.IF.State: Returns the number of "live" processes.
numMemoryUnits() - Method in interface dev.civl.mc.model.IF.contract.MemoryEvent: Returns the number of memory units associated with this event.
numProcs() - Method in interface dev.civl.mc.state.IF.State: Returns the number of process states in this state.
numReadsMemoryUnits() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the number of reads clauses of this behavior.
numRequirements() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Returns the number of preconditions of this behavior.
numStatesExplored() - Method in class dev.civl.mc.kripke.IF.CIVLStateManager
numVariables() - Method in interface dev.civl.mc.model.IF.Scope

O

objectType() - Method in interface dev.civl.mc.model.IF.expression.MemoryUnitExpression
OMP - Static variable in class dev.civl.mc.config.IF.CIVLConstants
OMP_LOOP_DECOMP - Static variable in class dev.civl.mc.config.IF.CIVLConstants
OMP_NO_SIMPLIFY - Static variable in class dev.civl.mc.config.IF.CIVLConstants
OMP_ONLY_SIMPLIFIER - Static variable in class dev.civl.mc.config.IF.CIVLConstants
OMP_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
ompLoopDecomp() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
ompLoopDecompO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Set the loop decomposition strategy for OpenMP transformer.
ompNoSimplify() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
ompNoSimplifyO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Don't simplify OpenMP pragmas? false by default.
ompOnlySimplifier() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
ompOnlySimplifierO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Only relies on the OpenMP simplifier ? i.e., either simplify an omp program or report possible data-race
OP - Static variable in class dev.civl.mc.config.IF.CIVLConstants
OpenMP2CIVLTransformer - Class in dev.civl.mc.transform.IF: OpenMP2CIVLTransformer transforms an AST of an OpenMP program into an AST of an equivalent CIVL-C program.
OpenMP2CIVLTransformer(ASTFactory, CIVLConfiguration) - Constructor for class dev.civl.mc.transform.IF.OpenMP2CIVLTransformer: Creates a new instance of OpenMP2CIVLTransformer.
OpenMPSimplifier - Class in dev.civl.mc.transform.IF: This transformer analyzes OpenMP constructs and converts them to simpler, i.e., less concurrent, instances of constructs.
OpenMPSimplifier(ASTFactory, CIVLConfiguration) - Constructor for class dev.civl.mc.transform.IF.OpenMPSimplifier
operand() - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression
operand() - Method in interface dev.civl.mc.model.IF.expression.UnaryExpression
operator() - Method in interface dev.civl.mc.model.IF.contract.CompositeEvent: Returns the operator.
operator() - Method in interface dev.civl.mc.model.IF.expression.BinaryExpression
operator() - Method in interface dev.civl.mc.model.IF.expression.UnaryExpression
operatorToString() - Method in interface dev.civl.mc.model.IF.expression.BinaryExpression
operatorToString() - Method in interface dev.civl.mc.model.IF.expression.UnaryExpression
OR - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
OTHER - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
out() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
OUT_OF_BOUNDS - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
outerScope() - Method in interface dev.civl.mc.model.IF.CIVLFunction
outgoing() - Method in interface dev.civl.mc.model.IF.location.Location
outptutNames() - Method in class dev.civl.mc.kripke.IF.CIVLStateManager: The names of output variables of the model.
OUTPUT_READ - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
outputVariables() - Method in interface dev.civl.mc.model.IF.Model: Return the output variables of this model, which all belong to the root scope.
overstrikeText(String) - Static method in class dev.civl.mc.util.IF.Utils

P

Pair<S,T> - Class in dev.civl.mc.util.IF
Pair(S, T) - Constructor for class dev.civl.mc.util.IF.Pair
PARALLEL_ASSIGN - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind: multiple assignments at a time
parallelAssignStatement(CIVLSource, List<Pair<LHSExpression, Expression>>) - Method in interface dev.civl.mc.model.IF.ModelFactory
ParallelAssignStatement - Interface in dev.civl.mc.model.IF.statement
parallelCombineWith(Fragment) - Method in interface dev.civl.mc.model.IF.Fragment: Combine this fragment and another fragment in parallel, i.e., merge the start location, and add the last statement of both fragments as the last statement of the result fragment
parameters() - Method in interface dev.civl.mc.model.IF.CIVLFunction
parameterTypes() - Method in interface dev.civl.mc.model.IF.type.CIVLFunctionType
parent - Variable in class dev.civl.mc.util.IF.SeqSet.Node: The parent node in the tree, or null if this is the root.
parent() - Method in interface dev.civl.mc.model.IF.Scope
parentPointer(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility: Given a non-trivial pointer, i.e., a pointer to some location inside an object, returns the parent pointer.
parProcFunction() - Method in interface dev.civl.mc.model.IF.statement.CivlParForSpawnStatement: returns the function to be executed by the spawned processes, which is equivalent to the body of the $parfor.
parProcsVar() - Method in interface dev.civl.mc.model.IF.statement.CivlParForSpawnStatement: returns the variable that represents the array of process references of processes spawned by this CivlParForSpawnStatement.
parProcsVariable(CIVLSource, CIVLType, Scope) - Method in interface dev.civl.mc.model.IF.ModelFactory
PARTIAL_ORDER - Enum constant in enum class dev.civl.mc.model.IF.AbstractFunction.SpecialRelationKind: this abstract function represents a partial order binary relation
partials() - Method in interface dev.civl.mc.model.IF.expression.DerivativeCallExpression
pathCondition() - Method in interface dev.civl.mc.model.IF.location.Location: returns the path condition of this location from the start location
pathconditionToString(CIVLSource, State, String, BooleanExpression) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer: Pretty representation of a path condition, which is broken into lines if it is in CNF.
peekReadWriteSet(State, int, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory
peekSecondLastStack() - Method in interface dev.civl.mc.state.IF.ProcessState: Returns the second top frame on the call stack.
peekStack() - Method in interface dev.civl.mc.state.IF.ProcessState: Returns the top frame on the call stack.
pid() - Method in interface dev.civl.mc.semantics.IF.Transition: The PID of the process that this transition belongs to.
PIECEWISE_LINEAR_ORDER - Enum constant in enum class dev.civl.mc.model.IF.AbstractFunction.SpecialRelationKind: this abstract function represents a piecewise linear order binary relation
PLUS - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
pointer() - Method in interface dev.civl.mc.model.IF.expression.DereferenceExpression: Returns the sole argument of this dereference expression.
POINTER - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
POINTER - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
POINTER - Enum constant in enum class dev.civl.mc.semantics.IF.Format.ConversionType
POINTER - Static variable in class dev.civl.mc.config.IF.CIVLConstants
POINTER_ADD - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
POINTER_SUBTRACT - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR
pointerArithmetics(CIVLSource, State, boolean, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.SymbolicAnalyzer
pointerSubtraction(State, int, String, BinaryExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.mc.semantics.IF.Evaluator: Evaluation pointer subtraction.
pointerSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the symbolic type used to represent pointers.
pointerToHeapVidMap() - Method in interface dev.civl.mc.model.IF.LogicFunction
pointerType(CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get a new pointer type.
popAssumption(State, int) - Method in interface dev.civl.mc.state.IF.StateFactory
popCallStack(State, int) - Method in interface dev.civl.mc.state.IF.StateFactory: Pops an entry off the call stack for a process.
popReadWriteSet(State, int, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory
POTENTIAL - Enum constant in enum class dev.civl.mc.config.IF.CIVLConstants.DeadlockKind
PotentialDeadlock - Interface in dev.civl.mc.predicate.IF: An potential deadlock occurs if all of the following hold: not every process has terminated the only enabled transitions are sends for which there is no matching receive
Predicates - Class in dev.civl.mc.predicate.IF
Predicates() - Constructor for class dev.civl.mc.predicate.IF.Predicates
PREEMPTION_BOUND - Static variable in class dev.civl.mc.config.IF.CIVLConstants
preemptionBound() - Method in class dev.civl.mc.config.IF.CIVLConfiguration: An upper bound on the number of preemptions allowed in an execution.
preemptionBoundO - Static variable in class dev.civl.mc.config.IF.CIVLConstants
PREFIX - Static variable in class dev.civl.mc.transform.IF.GeneralTransformer
PREFIX - Static variable in class dev.civl.mc.transform.IF.ShortCircuitTransformer
PREPROC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
preprocO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Show the preprocessing result? false by default.
PRIMITIVE - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind
primitiveTypeKind() - Method in interface dev.civl.mc.model.IF.type.CIVLPrimitiveType
print(PrintStream) - Method in interface dev.civl.mc.model.IF.CIVLSource: Prints the source to print stream.
print(PrintStream) - Method in interface dev.civl.mc.model.IF.Fragment: Print the fragment
print(PrintStream) - Method in interface dev.civl.mc.state.IF.MemoryUnit
print(PrintStream) - Method in interface dev.civl.mc.state.IF.MemoryUnitSet
print(PrintStream) - Method in interface dev.civl.mc.state.IF.State: Prints the state to a given print stream.
print(PrintStream) - Method in interface dev.civl.mc.util.IF.Printable: Print something to the given output stream.
print(PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.Model: Print the model.
print(PrintStream, String) - Method in interface dev.civl.mc.state.IF.DynamicScope: Prints a human-readable representation of this dynamic scope.
print(PrintStream, String) - Method in interface dev.civl.mc.state.IF.ProcessState: Prints a human-readable form of this process state.
print(String, PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.CIVLFunction: Print the function.
print(String, PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior: Prints this behavior
print(String, PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.contract.FunctionContract: prints this function contract
print(String, PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.contract.NamedFunctionBehavior: prints this behavior
print(String, PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.location.Location: Print this location and all outgoing transitions.
print(String, PrintStream, boolean) - Method in interface dev.civl.mc.model.IF.Scope: Print the scope and all children.
Printable - Interface in dev.civl.mc.util.IF: An object supporting a "print" method.
printAnalysis(PrintStream) - Method in interface dev.civl.mc.analysis.IF.CodeAnalyzer: Print the results the analyzer.
printBody(PrintStream) - Method in class dev.civl.mc.log.IF.CIVLLogEntry
printf(PrintStream, CIVLSource, String, List<Format>, List<StringBuffer>) - Method in interface dev.civl.mc.semantics.IF.Executor: If there are insufficient arguments for the format, the behavior is undefined.
printResults(List<CodeAnalyzer>, PrintStream) - Static method in class dev.civl.mc.analysis.IF.Analysis: prints the analysis result of each code analyzer.
printStates() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
printTransitions() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
printUnreachedCode(PrintStream) - Method in interface dev.civl.mc.model.IF.Model: prints the unreached code of the model
printUpdate() - Method in class dev.civl.mc.kripke.IF.CIVLStateManager: Print an update message at your earliest possible convenience.
prob() - Method in class dev.civl.mc.config.IF.CIVLConfiguration
PROB - Static variable in class dev.civl.mc.config.IF.CIVLConstants
problem() - Method in class dev.civl.mc.log.IF.CIVLLogEntry
probO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Use probabilistic techniques for verifying numeric identifies.
PROC_BOUND - Static variable in class dev.civl.mc.config.IF.CIVLConstants
PROC_NULL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
PROC_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the name of process reference type
procBoundO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: The bound on number of live processes (no bound if negative).
PROCESS - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind
PROCESS_LEAK - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty
processIdentifier() - Method in interface dev.civl.mc.kripke.IF.TraceStep: Returns the identifier of the process that this trace step belongs to.
processInAtomic(State) - Method in interface dev.civl.mc.state.IF.StateFactory: Returns the PID of the process that holds the atomic lock at a certain state
ProcessState - Interface in dev.civl.mc.state.IF: A ProcessState represents the state of a process (thread of execution) in a CIVL model.
processSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Returns the symbolic type used to represent process reference values
processType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory: Get the process type.
processValue(int) - Method in interface dev.civl.mc.state.IF.StateFactory
procnullExpression(CIVLSource) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates a $proc_null constant expression.
ProcnullExpression - Interface in dev.civl.mc.model.IF.expression
program() - Method in interface dev.civl.mc.model.IF.Model
property - Variable in exception class dev.civl.mc.state.IF.CIVLStateException
PROVEABLE - Enum constant in enum class dev.civl.mc.model.IF.CIVLException.Certainty: A theorem prover says this is an error: second-highest level of certainty.
PTHREAD - Static variable in class dev.civl.mc.config.IF.CIVLConstants
PTHREAD_GPOOL - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of _pthread_gpool_t type, which is the object type of the handle $pthread_gpool, and is used by pthread.cvl.
PTHREAD_POOL - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of _pthread_poo_t type, which is the object type of the handle $pthread_pool, and is used by pthread.cvl.
PTHREAD_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants
PTHREAD_THREAD_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: The name of the "pthread_t" type defined in pthread library
Pthread2CIVLTransformer - Class in dev.civl.mc.transform.IF
Pthread2CIVLTransformer(ASTFactory) - Constructor for class dev.civl.mc.transform.IF.Pthread2CIVLTransformer
purelyLocal() - Method in interface dev.civl.mc.model.IF.variable.Variable: return true iff the variable is purely local, i.e., v is purely local if there is no invalid input: '&v' in the model, and in v's scope, if there are no spawned functions that refer to v
purelyLocalAnalysis() - Method in interface dev.civl.mc.model.IF.CIVLFunction: performs purely local analysis one each statement/location of this function, and concludes if the whole function is purely local or not.
purelyLocalAnalysis() - Method in interface dev.civl.mc.model.IF.expression.Expression: Analyzes if this expression is purely local
purelyLocalAnalysis() - Method in interface dev.civl.mc.model.IF.location.Location: Analyze if the location is purely local
purelyLocalAnalysisForVariables() - Method in interface dev.civl.mc.model.IF.CIVLFunction: performs purely local analysis on variables for each statement/location of this function.
purelyLocalAnalysisOfVariables(Scope) - Method in interface dev.civl.mc.model.IF.expression.Expression: Analyzes if variables accessed by this expression are purely local
purelyLocalAnalysisOfVariables(Scope) - Method in interface dev.civl.mc.model.IF.statement.Statement: if an invalid input: '&'(var) is encountered, then var is considered as no purely local if a statement inside a function with fscope is accessing some variable that is declared in the scope vscope such that fscope.isDescendantOf(vscope), then that variable is not purely local
PURPLE - Enum constant in enum class dev.civl.mc.util.IF.Utils.Color
pushAssumption(State, int, BooleanExpression) - Method in interface dev.civl.mc.state.IF.StateFactory
pushCallStack(State, int, CIVLFunction, int, SymbolicExpression[]) - Method in interface dev.civl.mc.state.IF.StateFactory: Pushes a new entry onto the call stack for a process.
pushCallStack(State, int, CIVLFunction, SymbolicExpression[]) - Method in interface dev.civl.mc.state.IF.StateFactory: Pushes a new entry onto the call stack for a process.
pushContract(State, int, CIVLFunction, SymbolicExpression[]) - Method in interface dev.civl.mc.state.IF.StateFactory: Pushes a new frame onto the call stack where static scope of the frame is the contract scope of a function.
pushEmptyReadWrite(State, int, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory

Q

quantifiedExpression(CIVLSource, QuantifiedExpression.Quantifier, List<Pair<List<Variable>, Expression>>, Expression, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory: Creates a new quantified expression.
QuantifiedExpression - Interface in dev.civl.mc.model.IF.expression: A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.
QuantifiedExpression.Quantifier - Enum Class in dev.civl.mc.model.IF.expression: The different kinds of quantifiers which are possible.
quantifier() - Method in interface dev.civl.mc.model.IF.expression.QuantifiedExpression
QUANTIFIER - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind
QUEUE_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration: the name of queue type
queueType() - Method in interface dev.civl.mc.model.IF.Model
QUIET - Static variable in class dev.civl.mc.config.IF.CIVLConstants
quietO - Static variable in class dev.civl.mc.config.IF.CIVLConstants: Ignore the output? false by default.

R

RANDOM - Static variable in class dev.civl.mc.config.IF.CIVLConstants

randomO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

RANGE_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

The name of the $range type.

range2BitSet(SymbolicExpression, Reasoner) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

pre-condition : The parameter range is either a range or an integer

rangeAt(int) - Method in interface dev.civl.mc.model.IF.expression.RecDomainLiteralExpression

Returns the range expression of the domain literal at the given index.

rangeType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory

Returns the range type of the system.

REACH - Enum constant in enum class dev.civl.mc.model.IF.contract.DependsEvent.DependsEventKind

reachable() - Method in interface dev.civl.mc.model.IF.statement.Statement

Returns true if the statement has been reached at least once during the verification.

reachableByProcess(int, int) - Method in interface dev.civl.mc.state.IF.State

Is this dynamic scope reachable by the process with the given PID?

reachableMemUnitsWoPointer() - Method in interface dev.civl.mc.model.IF.location.Location

reachableMemUnitsWtPointer() - Method in interface dev.civl.mc.model.IF.location.Location

reached() - Method in interface dev.civl.mc.model.IF.statement.Statement

Mark this statement as reached.

READ - Enum constant in enum class dev.civl.mc.model.IF.contract.DependsEvent.DependsEventKind

readsMemoryUnits() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Returns the reads clause of this behavior.

readsNothing() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Does this function reads nothing? That is, is there a reads \nothing; clause in the contract.

REAL - Enum constant in enum class dev.civl.mc.model.IF.expression.LiteralExpression.LiteralKind

REAL - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind

REAL_FILE_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

The file type $file.

REAL_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

realLiteralExpression(CIVLSource, BigDecimal) - Method in interface dev.civl.mc.model.IF.ModelFactory

A real literal expression.

RealLiteralExpression - Interface in dev.civl.mc.model.IF.expression

A real literal.

realType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory

Get the real primitive type.

REC_DOMAIN_LITERAL - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

recDomainHasNext(SymbolicExpression, int, List<SymbolicExpression>) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Check if the given domain element has a subsequence in the given rectangular domain.

recDomainLiteralExpression(CIVLSource, List<Expression>, CIVLType) - Method in interface dev.civl.mc.model.IF.ModelFactory

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

RecDomainLiteralExpression - Interface in dev.civl.mc.model.IF.expression

This is a rectangular domain literal expression, which is the Cartesian product of a number of ranges, e.g., {range1, range2, range3, ...}.

RED - Enum constant in enum class dev.civl.mc.util.IF.Utils.Color

reference() - Method in interface dev.civl.mc.model.IF.expression.MemoryUnitExpression

Returns the reference of this memory unit expression.

reference() - Method in interface dev.civl.mc.state.IF.MemoryUnit

The reference of the memory unit.

reference(State, int, LHSExpression) - Method in interface dev.civl.mc.semantics.IF.Evaluator

Creates a pointer value by evaluating a left-hand-side expression in the given state.

referenceOfPointer(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Computes the reference expression of a pointer.

referenceToHeapMemUnit(SymbolicExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Computes the reference expression of a given heap pointer w.r.t the corresponding heap object.

REG_RANGE - Enum constant in enum class dev.civl.mc.model.IF.expression.reference.ArraySliceReference.ArraySliceKind

REGULAR_RANGE - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

regularRangeExpression(CIVLSource, Expression, Expression, Expression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Creates a regular range expression, which has the syntax low ..

RegularRangeExpression - Interface in dev.civl.mc.model.IF.expression

Represents a CIVL-C regular range expression, which has the form lo ..

releaseAtomicLock(State) - Method in interface dev.civl.mc.state.IF.StateFactory

Releases the atomic lock, by updating the atomic lock variable with the undefined process value.

removeIncoming(Statement) - Method in interface dev.civl.mc.model.IF.location.Location

Remove a certain incoming statement

removeOutgoing(Statement) - Method in interface dev.civl.mc.model.IF.location.Location

Remove a certain outgoing statement

removeProcess(State, int) - Method in interface dev.civl.mc.state.IF.StateFactory

Removes a process from the state.

replaceWith(ConditionalExpression, Expression) - Method in interface dev.civl.mc.model.IF.expression.Expression

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

replaceWith(ConditionalExpression, Expression) - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

replaceWith(ConditionalExpression, Expression) - Method in interface dev.civl.mc.model.IF.statement.Statement

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.

replaceWith(ConditionalExpression, VariableExpression) - Method in interface dev.civl.mc.model.IF.expression.Expression

Replace a certain conditional expression with a variable expression.

replaceWith(ConditionalExpression, VariableExpression) - Method in interface dev.civl.mc.model.IF.statement.Statement

Modify this statement including its guard by replacing a certain conditional expression with a variable expression, used when translating away conditional expression and a temporal variable is introduced.
For example, x = a ? b : c will be translated into if(a) v0 = b; else v0 = c; x = v0;
Another example, $when(a?b:c) x = k; will be translated into if(a) v0 = b; else v0 = c; $when(v0) x = k;

requirements() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Returns the preconditions of this behavior.

REQUIRES - Enum constant in enum class dev.civl.mc.model.IF.contract.FunctionContract.ContractKind

RESERVE_NAMES - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

the set of reserved names for symbolic constants

RESERVED_PERMUT - Static variable in interface dev.civl.mc.model.IF.LogicFunction

A reserved logic function (int *a, int *b, int l, int h) : bool has a dynamic type (int a[], int oft_a, int b[], int oft_b, int l, int h) : bool after stateless transformation.

ReservedLogicFunctionNames - Static variable in interface dev.civl.mc.model.IF.LogicFunction

Reserved logic functions are defined by CIVL/SARL

restriction() - Method in interface dev.civl.mc.model.IF.expression.ArrayLambdaExpression

Boolean-valued expression assumed to hold when evaluating expression.

restriction() - Method in interface dev.civl.mc.model.IF.expression.QuantifiedExpression

Boolean-valued expression assumed to hold when evaluating expression.

RESULT - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

RETURN - Enum constant in enum class dev.civl.mc.model.IF.statement.Statement.StatementKind

Return statement

returnFragment(CIVLSource, Location, Expression, CIVLFunction) - Method in interface dev.civl.mc.model.IF.ModelFactory

Create a one-statement fragment that contains the return statement.

ReturnStatement - Interface in dev.civl.mc.model.IF.statement

A return statement.

returnType() - Method in interface dev.civl.mc.model.IF.CIVLFunction

returnType() - Method in interface dev.civl.mc.model.IF.type.CIVLFunctionType

rhs() - Method in interface dev.civl.mc.model.IF.statement.AssignStatement

right - Variable in class dev.civl.mc.util.IF.Pair

right() - Method in interface dev.civl.mc.model.IF.contract.CompositeEvent

Returns the right operand

right() - Method in interface dev.civl.mc.model.IF.expression.BinaryExpression

ROOT_RESOURCE_PATH_STR - Static variable in class dev.civl.mc.config.IF.CIVLConstants

The common root of the paths of all resources.

rootDyscopeID() - Method in interface dev.civl.mc.state.IF.State

Returns the dynamic scope ID of the root (or "system") scope.

rootFunction() - Method in interface dev.civl.mc.model.IF.Model

run(String) - Method in class dev.civl.mc.run.IF.UserInterface

Runs command specified as one big String.

run(String...) - Method in class dev.civl.mc.run.IF.UserInterface

Runs the appropriate CIVL tools based on the command line arguments.

run(Collection<String>) - Method in class dev.civl.mc.run.IF.UserInterface

Runs the appropriate CIVL tools based on the command line arguments.

RUNTIME_UPDATE - Static variable in class dev.civl.mc.config.IF.CIVLConstants

runtimeUpdate() - Method in class dev.civl.mc.config.IF.CIVLConfiguration

runtimeUpdateO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

set false to disable CIVL

invalid reference

UpdaterRunnable

thread.

S

SAVE_STATES - Static variable in class dev.civl.mc.config.IF.CIVLConstants

saveStates() - Method in class dev.civl.mc.config.IF.CIVLConfiguration

saveStatesO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Save states during depth-first search? true by default.

SCHED - Static variable in class dev.civl.mc.config.IF.CIVLConstants

SCHED_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants

scope() - Method in interface dev.civl.mc.model.IF.contract.FunctionContract

The static scope in which the function contract exists.

scope() - Method in interface dev.civl.mc.model.IF.expression.FunctionIdentifierExpression

scope() - Method in interface dev.civl.mc.model.IF.location.Location

scope() - Method in interface dev.civl.mc.model.IF.variable.Variable

scope() - Method in interface dev.civl.mc.state.IF.StackEntry

scope(CIVLSource, Scope, List<Variable>, CIVLFunction) - Method in interface dev.civl.mc.model.IF.ModelFactory

Create a new scope.

Scope - Interface in dev.civl.mc.model.IF

A scope.

SCOPE - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind

SCOPE - Static variable in class dev.civl.mc.config.IF.CIVLConstants

SCOPE_TYPE - Static variable in class dev.civl.mc.model.IF.ModelConfiguration

scopeId() - Method in interface dev.civl.mc.model.IF.expression.MemoryUnitExpression

Returns the (static) scope id of the variable.

scopeIdentityToValueOperator(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLScopeType

SCOPEOF - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

scopeofExpression(CIVLSource, LHSExpression) - Method in interface dev.civl.mc.model.IF.ModelFactory

Creates a new $scopeof expression using the given argument.

ScopeofExpression - Interface in dev.civl.mc.model.IF.expression

A scopeof expression is "$scopeof(expr)".

scopes() - Method in interface dev.civl.mc.model.IF.CIVLFunction

scopeSymbolicType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory

Returns the symbolic type used to represent scope values

scopeType() - Method in interface dev.civl.mc.model.IF.CIVLTypeFactory

Get the scope primitive type.

scopeValue() - Method in interface dev.civl.mc.model.IF.type.CIVLMemType.MemoryLocationReference

The scope value of the scope where the corresponding variable declared

scopeValue(int) - Method in interface dev.civl.mc.state.IF.StateFactory

Converts an integer dynamic scope id into a symbolic expression

scopeValueToIdentityOperator(SymbolicUniverse) - Method in interface dev.civl.mc.model.IF.type.CIVLScopeType

second - Variable in class dev.civl.mc.util.IF.Triple

SEED - Static variable in class dev.civl.mc.config.IF.CIVLConstants

seedO - Static variable in class dev.civl.mc.config.IF.CIVLConstants

Set the random seed for run mode.

select(String) - Static method in enum class dev.civl.mc.config.IF.CIVLConstants.MPIModelKind

maps string literal option value to CIVLConstants.MPIModelKind.

selectScopeValuesMap(SymbolicUniverse, SymbolicExpression) - Method in interface dev.civl.mc.model.IF.type.CIVLStateType

Extract the scope value mapper from an object of the CIVLStateType.

selectStateKey(SymbolicUniverse, SymbolicExpression) - Method in interface dev.civl.mc.model.IF.type.CIVLStateType

Extracts the integral key from an object of CIVLStateType.

SELF - Enum constant in enum class dev.civl.mc.model.IF.expression.Expression.ExpressionKind

SELF - Enum constant in enum class dev.civl.mc.model.IF.expression.reference.MemoryUnitReference.MemoryUnitReferenceKind

selfExpression(CIVLSource) - Method in interface dev.civl.mc.model.IF.ModelFactory

A self expression.

SelfExpression - Interface in dev.civl.mc.model.IF.expression

Self expression.

selfReference() - Method in interface dev.civl.mc.model.IF.ModelFactory

SelfReference - Interface in dev.civl.mc.model.IF.expression.reference

This represents the complete reference to a variable.

Semantics - Class in dev.civl.mc.semantics.IF

Entry point of the module civl.semantics.

Semantics() - Constructor for class dev.civl.mc.semantics.IF.Semantics

SEQ - Static variable in class dev.civl.mc.config.IF.CIVLConstants

SEQ_SRC - Static variable in class dev.civl.mc.config.IF.CIVLConstants

SeqSet - Class in dev.civl.mc.util.IF

A SeqSet represents a set of sequences of nonnegative integers.

SeqSet() - Constructor for class dev.civl.mc.util.IF.SeqSet

Creates new empty set.

SeqSet.Node - Class in dev.civl.mc.util.IF

A node in the tree representation.

SEQUENCE - Enum constant in enum class dev.civl.mc.model.IF.CIVLProperty

SET - Enum constant in enum class dev.civl.mc.model.IF.type.CIVLType.TypeKind

the type represents a set of a non-set kind CIVLTypes, see CIVLSetType

setAbsAnalysis(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setAccessesAtomicFunction(Set<Variable>) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setArguments(List<Expression>) - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

setArray(LHSExpression) - Method in interface dev.civl.mc.model.IF.expression.SubscriptExpression

setAsRun(boolean) - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

Pre-condition: CallOrSpawnStatement.isSpawn() == true

setAssignToLeft(boolean) - Method in interface dev.civl.mc.model.IF.expression.BinaryExpression

setAssingsNothing() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

When a assigns \nothing; clause appears, sets the function behavior to be assigning nothing.

setAsStart(boolean) - Method in interface dev.civl.mc.model.IF.location.Location

setAssumption(Expression) - Method in interface dev.civl.mc.model.IF.contract.NamedFunctionBehavior

Set the conjunction of all assumptions to this behavior.

setBinaryBranching(boolean) - Method in interface dev.civl.mc.model.IF.location.Location

update this location to denote if it is a binary branching location

setBundleType(CIVLBundleType) - Method in interface dev.civl.mc.model.IF.Model

updates the bundle type of the model

setCheckDeadlockKind(CIVLConstants.DeadlockKind) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

Sets the kind of deadlocks we want to check for

setCheckExpressionError(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setChild(int) - Method in class dev.civl.mc.util.IF.SeqSet.Node

If this node already contains the child at index, does nothing and returns false.

setChildren(Set<Scope>) - Method in interface dev.civl.mc.model.IF.Scope

setCIVLSource(CIVLSource) - Method in interface dev.civl.mc.model.IF.Sourceable

setCIVLSource(CIVLSource) - Method in interface dev.civl.mc.model.IF.statement.Statement

setCodeAnalyzers(List<CodeAnalyzer>) - Method in interface dev.civl.mc.model.IF.ModelFactory

setCollectHeaps(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setCollectOutputs(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setCollectProcesses(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setCollectScopes(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setCollectSymbolicNames(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setConfiguration(CIVLConfiguration) - Method in interface dev.civl.mc.semantics.IF.Evaluator

setConfiguration(CIVLConfiguration) - Method in interface dev.civl.mc.semantics.IF.Executor

setConfiguration(CIVLConfiguration) - Method in interface dev.civl.mc.state.IF.StateFactory

setConst(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

setConstantValue(SymbolicExpression) - Method in interface dev.civl.mc.model.IF.variable.Variable

sets the constant value of this variable

setConstantValue(ProverFunctionInterpretation) - Method in interface dev.civl.mc.model.IF.LogicFunction

Caching the evaluation of a logic function since the definition of a logic function is suppose to be stateless, there is no need to repeatedly evaluate it.

setContainingScope(Scope) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setDebug(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setDefaultBehavior(FunctionBehavior) - Method in interface dev.civl.mc.model.IF.contract.FunctionContract

Sets the default behavior of the function.

setDependsAnyact() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

When a depends \anyact; clause appears, sets the function behavior to be depending on anything.
Precondition:

invalid @link

{@link #dependsNoact()==false

};

setDependsNoact() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

When a depends \noact; clause appears, sets the function behavior to be depending on nothing.
Precondition: FunctionBehavior.numDependsEvents()==0 invalid input: '&'invalid input: '&' ==false;

setDirectSymEx(String) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setDpor(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setEnablePrintf(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setEnterAtomic() - Method in interface dev.civl.mc.model.IF.location.Location

This location is the start location of a certain atomic block

setEntryOfUnsafeAtomic(boolean) - Method in interface dev.civl.mc.model.IF.location.Location

Set the mark of atomic block termination.

setErr(PrintStream) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setErrorFree(boolean) - Method in interface dev.civl.mc.model.IF.expression.Expression

setErrorStateEquiv(CIVLConstants.ErrorStateEquivalence) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setEvaluator(Evaluator) - Method in interface dev.civl.mc.semantics.IF.LibraryExecutor

setExpression(Expression) - Method in interface dev.civl.mc.model.IF.statement.ReturnStatement

setExpressionType(CIVLType) - Method in interface dev.civl.mc.model.IF.expression.FunctionCallExpression

setExternVariables(Map<String, Variable>) - Method in interface dev.civl.mc.model.IF.Model

setFair(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setFieldIndex(int) - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression

setFieldOffset(boolean) - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression

setFinalState(State) - Method in interface dev.civl.mc.kripke.IF.TraceStep

Set final state to the trace step.

setFinalStatements(Set<Statement>) - Method in interface dev.civl.mc.model.IF.Fragment

Update the last statement of this fragment

setFreeOfUnsafeloop(boolean) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setFunction(CIVLFunction) - Method in interface dev.civl.mc.model.IF.contract.CallEvent

Sets the callee of this event

setFunction(CIVLFunction) - Method in interface dev.civl.mc.model.IF.Scope

setFunction(FunctionIdentifierExpression) - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

TODO: get rid of this, but updates the function expression instead.

setFunctionContract(FunctionContract) - Method in interface dev.civl.mc.model.IF.CIVLFunction

sets the contract of this function.

setFunctions(Set<CIVLFunction>) - Method in interface dev.civl.mc.model.IF.Model

setGuard(Expression) - Method in interface dev.civl.mc.model.IF.contract.FunctionContract

Sets the guard of the function.

setGuard(Expression) - Method in interface dev.civl.mc.model.IF.statement.Statement

setHandleObjectType(boolean) - Method in interface dev.civl.mc.model.IF.type.CIVLStructOrUnionType

Updates the option whether this type is the object type of some handle type, with the given value.

setHasFscanf(boolean) - Method in interface dev.civl.mc.model.IF.Model

updates the flag which denotes either the model contains any fscanf call or not.

setId(int) - Method in interface dev.civl.mc.model.IF.location.Location

Set the unique ID number of this location.

setImpactMemoryUnit(Set<MemoryUnitExpression>) - Method in interface dev.civl.mc.model.IF.location.Location

setImpactScopeOfAtomicOrAtomBlock(Scope) - Method in interface dev.civl.mc.model.IF.location.Location

set the impact scope of a location, only called when this.AtomicKind == ATOM_ENTER or ATOMIC_ENTER.

setIndex(Expression) - Method in interface dev.civl.mc.model.IF.expression.SubscriptExpression

setInputVariables(Map<String, Object>) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setInSubprogram(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setIntBit(int) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setIntOperationTransiformer(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setIsBound(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

setIsEntryOfLocalBlock(boolean) - Method in interface dev.civl.mc.model.IF.location.Location

setIsInput(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

setIsOutput(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

SETJMP - Static variable in class dev.civl.mc.config.IF.CIVLConstants

setLeaveAtomic() - Method in interface dev.civl.mc.model.IF.location.Location

This location is the end location of a certain atomic block

setLhs(LHSExpression) - Method in interface dev.civl.mc.model.IF.statement.CallOrSpawnStatement

setLibrary(String) - Method in interface dev.civl.mc.model.IF.SystemFunction

setLiteralConstantValue(SymbolicExpression) - Method in interface dev.civl.mc.model.IF.expression.LiteralExpression

Directly set a symbolic expression as value of this literal expression

setLiteralObject(CompoundLiteralExpression.CIVLCompoundLiteralObject) - Method in interface dev.civl.mc.model.IF.expression.CompoundLiteralExpression

Set CompoundLiteralExpression.CIVLCompoundLiteralObject of this expression.

setLocation(Location) - Method in interface dev.civl.mc.model.IF.contract.LoopContract

Set the location which identifies a loop statement.

setLocation(State, int, Location) - Method in interface dev.civl.mc.state.IF.StateFactory

Sets the location of a process.

setLocation(State, int, Location, boolean) - Method in interface dev.civl.mc.state.IF.StateFactory

Sets the location of a process.

setLocations(Set<Location>) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setLogic(boolean) - Method in interface dev.civl.mc.model.IF.CIVLFunction

Set weather this function is a logic function.

setLogicFunctions(List<LogicFunction>) - Method in interface dev.civl.mc.model.IF.Model

Adding all translated logic functions to the model

setLoopPossible(boolean) - Method in interface dev.civl.mc.model.IF.location.Location

During the translation of AST node into CIVL model, it is possible to know if a location with more than one incoming statement possible to be a loop location

setMaxProcs(int) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setMessageType(CIVLType) - Method in interface dev.civl.mc.model.IF.Model

setModel(Model) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setModel(Model) - Method in interface dev.civl.mc.model.IF.statement.Statement

setMpiContractFunction(String) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setMpiModel(CIVLConstants.MPIModelKind) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setName(Identifier) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setName(Identifier) - Method in interface dev.civl.mc.model.IF.variable.Variable

setName(String) - Method in interface dev.civl.mc.model.IF.Model

setOmpLoopDecomp(int) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setOmpNoSimplifier(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setOmpOnlySimplify(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setOperand(Expression) - Method in interface dev.civl.mc.model.IF.expression.UnaryExpression

setOperator(UnaryExpression.UNARY_OPERATOR) - Method in interface dev.civl.mc.model.IF.expression.UnaryExpression

setOut(PrintStream) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setOuterScope(Scope) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setParameters(List<Variable>) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setParameterTypes(CIVLType[]) - Method in interface dev.civl.mc.model.IF.CIVLFunction

updates the types of the parameters of this function

setParameterTypes(CIVLType[]) - Method in interface dev.civl.mc.model.IF.type.CIVLFunctionType

setParent(Scope) - Method in interface dev.civl.mc.model.IF.Scope

setParProcFunction(CIVLFunction) - Method in interface dev.civl.mc.model.IF.statement.CivlParForSpawnStatement

updates the function which will be executed by spawned processes.

setPathcondition(Expression) - Method in interface dev.civl.mc.model.IF.location.Location

setPointerRef(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

updates the pointer reference feature of this variable.

setPostState(State) - Method in interface dev.civl.mc.kripke.IF.AtomicStep

Updates the resulting state of this atomic step.

setPrimaryEvaluator(Evaluator) - Method in interface dev.civl.mc.semantics.IF.LibraryEvaluator

setProb(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setProcBound(int) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setProcessState(State, ProcessState) - Method in interface dev.civl.mc.state.IF.StateFactory

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.

setPure(boolean) - Method in interface dev.civl.mc.model.IF.contract.FunctionContract

Updates the contract to denote if it contains pure clause.

setPureFunction(Boolean) - Method in interface dev.civl.mc.model.IF.CIVLFunction

updates the property of this function to be pure

setPurelyLocal(boolean) - Method in interface dev.civl.mc.model.IF.expression.LHSExpression

Updates the flag of the expression denoting if it is purely local.

setPurelyLocal(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

sets this variable to be purely local according to the given value

setQueueType(CIVLType) - Method in interface dev.civl.mc.model.IF.Model

setQuiet(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setReachableMemUnitsWoPointer(Set<MemoryUnitExpression>) - Method in interface dev.civl.mc.model.IF.location.Location

setReachableMemUnitsWtPointer(Set<MemoryUnitExpression>) - Method in interface dev.civl.mc.model.IF.location.Location

setReadsNothing() - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

When a reads \nothing; clause appears, sets the function behavior to be reading nothing.

setReference(ReferenceExpression) - Method in interface dev.civl.mc.state.IF.MemoryUnit

updates the reference of this memory unit

setRemovable() - Method in interface dev.civl.mc.model.IF.statement.NoopStatement

setReplay(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setReported() - Method in exception class dev.civl.mc.log.IF.CIVLExecutionException

Set this error to be reported.

setReturnType(CIVLType) - Method in interface dev.civl.mc.model.IF.CIVLFunction

updates the return type of this function

setReturnType(CIVLType) - Method in interface dev.civl.mc.model.IF.type.CIVLFunctionType

setRootFunction(CIVLFunction) - Method in interface dev.civl.mc.model.IF.Model

setRuntimeUpdate(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setSafeLoop(boolean) - Method in interface dev.civl.mc.model.IF.location.Location

Mark if the loop is a safe loop.

setSaveStates(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setScope(Scope) - Method in interface dev.civl.mc.model.IF.location.Location

setScope(Scope) - Method in interface dev.civl.mc.model.IF.variable.Variable

setScopes(Scope) - Method in interface dev.civl.mc.model.IF.ModelFactory

Set the system scope, which is the root (static) scope of the model.

setScopes(Set<Scope>) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setShowAmpleSet(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowAmpleSetWtStates(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowAST(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowInputVars(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowMemoryUnits(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowModel(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowPreproc(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowProgram(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowSavedStates(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowStates(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowTime(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowTransitions(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setShowUnreach(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setSimplify(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setSleepLocation(Location) - Method in interface dev.civl.mc.model.IF.Model

setSource(Location) - Method in interface dev.civl.mc.model.IF.statement.Statement

setSourceTemp(Location) - Method in interface dev.civl.mc.model.IF.statement.Statement

updates the source location of this statement, but never add this statement to the outgoing set of the source location

setStartLocation(Location) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setStartLocation(Location) - Method in interface dev.civl.mc.model.IF.Fragment

Update the start location of this fragment

setStateFunction(boolean) - Method in interface dev.civl.mc.model.IF.CIVLFunction

updates the property of this function to be a state function

setStatelessPrintf(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setStatements(Set<Statement>) - Method in interface dev.civl.mc.model.IF.CIVLFunction

setStateVariable(Variable) - Method in interface dev.civl.mc.model.IF.type.CIVLType

Sets this type's state variable to the given variable

setStatic(boolean) - Method in interface dev.civl.mc.model.IF.variable.Variable

sets this variable to be static qualified according to the given value

setSwitchOrChooseWithDefault() - Method in interface dev.civl.mc.model.IF.location.Location

Marks this location as a switch or $choose statement location who has a 'default' case.

setSymbolicUtility(SymbolicUtility) - Method in interface dev.civl.mc.state.IF.StateFactory

setSymRef(SymbolicExpression, ReferenceExpression) - Method in interface dev.civl.mc.dynamic.IF.SymbolicUtility

Returns the pointer value obtained by replacing the symRef component of the given pointer value with the given symRef.

setSystemCalls(Set<CallOrSpawnStatement>) - Method in interface dev.civl.mc.model.IF.location.Location

setTarget(Location) - Method in interface dev.civl.mc.model.IF.statement.Statement

setTargetTemp(Location) - Method in interface dev.civl.mc.model.IF.statement.Statement

updates the target location of this statement, but never add this statement to the incoming set of the target location

setTimeout(int) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setToggleableProperty(CIVLProperty, boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

Sets a CIVLProperty to be toggleable and to be either turned on or off

setTokenFactory(TokenFactory) - Method in interface dev.civl.mc.model.IF.ModelFactory

Set the token factory

setType(CIVLType) - Method in interface dev.civl.mc.model.IF.variable.Variable

setTypeForOffset(CIVLType) - Method in interface dev.civl.mc.model.IF.expression.AddressOfExpression

setUnpreproc(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setUpdater(Printable) - Method in class dev.civl.mc.kripke.IF.CIVLStateManager

Set the field savedStates.

setValue(char) - Method in interface dev.civl.mc.model.IF.expression.CharLiteralExpression

Update the value of this char literal.

setValue(int, SymbolicExpression) - Method in interface dev.civl.mc.state.IF.DynamicScope

Sets the value assigned to the vid-th variable.

setValue(BigDecimal) - Method in interface dev.civl.mc.model.IF.expression.RealLiteralExpression

setValue(BigInteger) - Method in interface dev.civl.mc.model.IF.expression.IntegerLiteralExpression

setVariable(Variable) - Method in interface dev.civl.mc.model.IF.expression.VariableExpression

setVariable(State, int, int, SymbolicExpression) - Method in interface dev.civl.mc.state.IF.StateFactory

Updates the value assigned to a variable in the state.

setVariable(State, Variable, int, SymbolicExpression) - Method in interface dev.civl.mc.state.IF.StateFactory

Updates the value assigned to a variable in the state.

setVariables(Set<Variable>) - Method in interface dev.civl.mc.model.IF.Scope

setVerbose(boolean) - Method in class dev.civl.mc.config.IF.CIVLConfiguration

setVid(int) - Method in interface dev.civl.mc.model.IF.variable.Variable

setWaitsforList(Iterable<Expression>) - Method in interface dev.civl.mc.model.IF.contract.FunctionBehavior

Set an expression collection as the arguments set as the "waitsfor" clause.

SHIFTLEFT - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR

SHIFTRIGHT - Enum constant in enum class dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR

SHORT_DESCRIPTION - Static variable in class dev.civl.mc.transform.IF.AnnotationTransformer