All Classes Interface Summary Class Summary Enum Summary Exception Summary
| Class |
Description |
| AbstractFunction |
An abstract function is an uninterpreted mathematical function.
|
| AbstractFunctionCallExpression |
An expression representing a call of an abstract function.
|
| AccuracyAssumptionBuilder |
An accuracy assumption builder provides logic for determining additional
assumptions that should be added after an assumption involving an abstract
function call.
|
| AddressOfExpression |
This represents an address-of expression, which contains one operand, and has
the format: &x, where & is the address-of operator
and x is the operand.
|
| Analysis |
Entry point of the module civl.analysis.
|
| AndPredicate |
This represents a predicate in CNF, containing a number of predicates, called
clauses, i.e., p1 & p2 & ...
|
| ArrayCutter |
This interface provides methods for dealing with array slices, e.g.
|
| ArrayLambdaExpression |
A CIVL-C quantified expression, including three components, bound variable
declaration list, (optional) restriction and expression.
|
| ArrayLiteralExpression |
|
| ArrayReshaper |
This class provides methods for reshaping arrays.
|
| ArraySliceReference |
This represents the reference to an array, which could be:
element
wildcard
range
|
| ArraySliceReference.ArraySliceKind |
|
| ArrayToolBox |
This interface provides a collection of methods that manipulating symbolic
expressions whose symbolic type has ARRAY kind.
|
| ArrayToolBox.ArrayShape |
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 |
the data structure for describing array slices.
|
| AssignStatement |
An assignment statement.
|
| AtomicLockAssignStatement |
|
| AtomicStep |
This represents an atomic execution step, which represents the execution of
exactly one transition.
|
| BinaryExpression |
A binary operation.
|
| BinaryExpression.BINARY_OPERATOR |
This defines all CIVL binary operators:
AND: && (logical and);
LEFT_SHIFT: < (bitwise left shift);
RIGHT_SHIFT: >> (bitwise right shift);
BITAND: & (bitwise and);
BITCOMPLEMENT: ~ (bitwise complement);
BITOR: | (bitwise or);
BITXOR: ^ (bitwise xor);
DIVIDE: / (division);
EQUAL: == (equal to);
IMPLIES: < (less than);
LESS_THAN_EQUAL: <= (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);
|
| BooleanLiteralExpression |
A literal boolean value.
|
| BoundVariableExpression |
A bound variable is a variable used in a quantified expression.
|
| BranchConstraints |
|
| CallEvent |
This represents a function call event of a depends clause.
|
| CallOrSpawnStatement |
A function call or spawn.
|
| CastExpression |
A cast of an expression to a different type.
|
| CharLiteralExpression |
|
| CIVL |
The main CIVL class, containing the main method, which provides the command
line interface for using CIVL.
|
| CIVLArrayType |
The type for an array of T.
|
| CIVLBundleType |
|
| CIVLCompleteArrayType |
The type for an array of T where the extent is specified.
|
| CIVLCompleteDomainType |
|
| CIVLConfiguration |
A CIVLConfiguration object encompasses all the parameters used to configure
CIVL for the execution of one or more tasks.
|
| CIVLConstants |
This class manages all constant configurations of the system.
|
| CIVLConstants.DeadlockKind |
Kinds of deadlock: absolute, potential or none.
|
| CIVLConstants.ErrorStateEquivalence |
Error state equivalence semantics for suppressing logging of redundant
errors.
|
| CIVLDomainType |
This is the only one CIVLDomainType associated to the $domain type in
program.
|
| CIVLEnumType |
An enumeration type.
|
| CIVLErrorLogger |
CIVLErrorLogger logs all errors of the system.
|
| CIVLException |
Root of CIVL exception hierarchy, representing any kind of event where
something goes wrong in CIVL.
|
| CIVLException.Certainty |
A certainty level gages how certain we are that this is error is a real
error, i.e., not just a spurious error.
|
| CIVLException.ErrorKind |
|
| CIVLExecutionException |
This represents an error during the execution of a program.
|
| CIVLFunction |
A CIVL function.
|
| CIVLFunctionType |
|
| CIVLHeapException |
Extends an execution exception with a state at which error occurred.
|
| CIVLHeapException.HeapErrorKind |
|
| CIVLHeapType |
|
| CIVLInternalException |
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.
|
| CIVLLogEntry |
This represents an entry in the error log of CIVL.
|
| CIVLMemType |
A CIVLType representing a set of memory locations. |
| CIVLMemType.MemoryLocationReference |
|
| CivlParForSpawnStatement |
This represents the first part of a $parfor construct, i.e., spawning
processes according the specified domain.
|
| CIVLPointerType |
Type of a pointer.
|
| CIVLPrimitiveType |
A primitive type is a type of which there is only one instance.
|
| CIVLPrimitiveType.PrimitiveTypeKind |
|
| CIVLRegularRangeType |
|
| CIVLScopeType |
The $scope type in the CIVL-C language.
|
| CIVLSetType |
A CIVLType representing a set of a non-set kind CIVLType. |
| CIVLSource |
A CIVLSource object represents a range of text in a source file.
|
| CIVLStateException |
Extends an execution exception with a state at which error occurred.
|
| CIVLStateManager |
StateManager extends StateManager for CIVL models.
|
| CIVLStatePredicate |
|
| CIVLStateType |
|
| CIVLStructOrUnionType |
Represents a "record" type (i.e.
|
| CIVLSyntaxException |
An exception thrown when there is syntax error in the program being verified,
e.g., calling $choose_int with more than one arguments, etc.
|
| CIVLType |
Parent of all types.
|
| CIVLType.TypeKind |
|
| CIVLTypeFactory |
The CIVL type factory provides the CIVL primitive types, like
$bool, int, float, $scope
, etc.
|
| CIVLUnimplementedFeatureException |
An exception thrown when there is not necessarily anything wrong with the
program begin verified, but some CIVL feature has not yet been implemented.
|
| CodeAnalyzer |
This represents a code analyzer for analyzing source code for a certain
property.
|
| CommandLine |
A command line represents the command line information for running CIVL.
|
| CommandLine.CommandLineKind |
CIVL command line kinds: normal, or compare.
|
| CommandLine.CommandName |
This contains the names of all commands supported by CIVL, either it is a
normal command or a compare command.
|
| CompositeEvent |
This represents a composite event, which could be a
union/difference/intersect of another two depends events.
|
| CompositeEvent.CompositeEventOperator |
|
| ConditionalExpression |
The ternary conditional expression ("?" in C).
|
| ContractFactory |
This factory is to create new instances of function contract components.
|
| ContractTransformer |
|
| Cuda2CIVLTransformer |
|
| Deadlock |
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).
|
| DependsEvent |
This represents an event which is used as one argument of the
depends clause.
|
| DependsEvent.DependsEventKind |
|
| DereferenceExpression |
|
| DerivativeCallExpression |
An uninterpreted call to the derivative of an abstract function.
|
| DifferentiableExpression |
This expression encodes the claim that a real, abstract function is
differentiable.
|
| DirectingTransformer |
This transformer instruments the model so as to direct
the symbolic execution down a subset of program paths.
|
| DomainGuardExpression |
This is the guard expression of CIVL for loops ($for).
|
| DomainIteratorStatement |
Updates the loop variables with the next element of a domain.
|
| DominatorAnalysis<E> |
This analysis uses an iterative fixed-point
data flow framework to find the dominators of
any node in a graph.
|
| DotExpression |
A dot expression is a reference to a field in a struct or union.
|
| DynamicMemoryLocationSet |
This class is a immutable data structure that stores a set of memory
locations.
|
| DynamicMemoryLocationSetFactory |
|
| Dynamics |
Entry point of the module dynamic.
|
| DynamicScope |
A DynamicScope is a runtime instance of a static scope.
|
| DynamicTypeOfExpression |
A "DynamicTypeOf" expression.
|
| Enabler |
Enabler extends EnablerIF for CIVL models.
|
| Evaluation |
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.
|
| Evaluator |
This is the CIVL main evaluator.
|
| Executor |
|
| Expression |
The parent of all expressions.
|
| Expression.ExpressionKind |
|
| ExtendedQuantifiedExpression |
The representation for the "fold expression" in ACSL, e.g.
|
| Format |
|
| Format.ConversionType |
|
| Fragment |
A fragment is a sequence of statements.
|
| FunctionalEquivalence |
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 |
This represents a non-named behavior of the ACSL function contract.
|
| FunctionCallExpression |
|
| FunctionContract |
This represents a block of ACSL contract for a function.
|
| FunctionContract.ContractKind |
ContractKind: This kind is used to denotes all kinds of contracts.
|
| FunctionGuardExpression |
A function guard expression is the guard expression of a function
call with a function pointer.
|
| FunctionIdentifierExpression |
|
| GeneralTransformer |
|
| HereOrRootExpression |
|
| Identifier |
An identifier.
|
| InitialValueExpression |
An expression yielding the initial value of a variable.
|
| IntegerLiteralExpression |
An integer literal.
|
| IntOperationTransformer |
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
|
| IOTransformer |
The IO transformer transforms
all function calls printf(...) into frpintf(stdout, ...)
all function calls scanf(...) into fscanf(stdin, ...)
all function calls fopen(...) into $fopen(...)
|
| Kripkes |
This is the entry point of the module kripke.
|
| LambdaExpression |
A CIVL-C quanti, bound variable declaration list, (optional) restriction and
expression.
|
| LHSExpression |
A left-hand-side expression.
|
| LHSExpression.LHSExpressionKind |
|
| LibraryEnabler |
A Library Enabler provides a method to compute the enabled transitions of
system function calls at a certain state for a give process.
|
| LibraryEnablerLoader |
The library enabler loader provides the mechanism for loading the library
enabler of a certain library.
|
| LibraryEvaluator |
A Library Evaluator provides a method to "evaluate" the guard of each system
function call.
|
| LibraryEvaluatorLoader |
The library evaluator loader provides the mechanism for loading the library
evaluator of a certain library.
|
| LibraryExecutor |
A Library Executor provides the semantics for system functions defined in a
library.
|
| LibraryExecutorLoader |
The library executor loader provides the mechanism for loading the library
executor of a certain library.
|
| LibraryLoaderException |
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.
|
| LiteralExpression |
The parent of all literal expressions.
|
| LiteralExpression.LiteralKind |
|
| Location |
The parent of all locations.
|
| Location.AtomicKind |
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.
|
| LogicFunction |
A logic function is a function whose definition (body) is either absent (i.e.
|
| LoopBranchStatement |
|
| LoopContract |
This class represents a group of loop annotations for a loop, including loop
invariants, loop assigns and loop variants.
|
| LoopContractTransformer |
|
| MacroTransformer |
|
| MallocStatement |
A statement for dynamic allocation of objects.
|
| MemoryEvent |
This represents a \read or \write event of a
depends clause.
|
| MemoryUnit |
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.
|
| MemoryUnitExpression |
A memory unit expression is an expression that represents (part of) the
memory related to some variable.
|
| MemoryUnitExpressionEvaluator |
|
| MemoryUnitFactory |
|
| MemoryUnitReference |
|
| MemoryUnitReference.MemoryUnitReferenceKind |
|
| MemoryUnitSet |
A memory unit set represents a set of memory units.
|
| Model |
A model of a CIVL program.
|
| ModelBuilder |
Class to provide translation from an AST to a model.
|
| ModelConfiguration |
This file contains the constants used by the model builder/translator, which
reflects the translation strategy of CIVL.
|
| ModelFactory |
The factory to create all model components.
|
| Models |
This is the entry point of the module model.
|
| ModelTranslator |
A model translator parses, links, transforms a sequence of source files (C or
CIVL-C programs) into a ABC program; and then build a CIVL model from that
program.
|
| MPI2CIVLTransformer |
MPI2CIVLTransformer transforms an AST of an MPI program into an AST of an
equivalent CIVL-C program.
|
| MPICollectiveBehavior |
|
| MPICollectiveBehavior.MPICommunicationPattern |
|
| MPIContractExpression |
This class represents a set of MPI contract expressions:
\mpi_empty_in: expresses that a receiving buffer is empty.
\mpi_empty_out: expresses that a sending buffer is empty.
\mpi_agree: expresses that an variable is same at the beginning for all
processes.
\mpi_equals: expresses that two pointers are pointing to the equal
obejects.
\mpi_region: represents an memory object in an MPI program.
|
| MPIContractExpression.MPI_CONTRACT_EXPRESSION_KIND |
|
| NamedFunctionBehavior |
A named behavior contains a name and assumptions in addition to those
components contained by FunctionBehavior. |
| NoopStatement |
Marker interface for a noop statement.
|
| NoopStatement.NoopKind |
|
| Nothing |
|
| OpenMP2CIVLTransformer |
OpenMP2CIVLTransformer transforms an AST of an OpenMP program into an AST of
an equivalent CIVL-C program.
|
| OpenMPOrphanTransformer |
|
| OpenMPSimplifier |
This transformer analyzes OpenMP constructs and converts them to simpler,
i.e., less concurrent, instances of constructs.
|
| Pair<S,T> |
|
| ParallelAssignStatement |
|
| Player |
Base class for various tools that require executing a CIVL model.
|
| PotentialDeadlock |
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 |
|
| Printable |
An object supporting a "print" method.
|
| ProcessState |
A ProcessState represents the state of a process (thread of execution) in a
CIVL model.
|
| ProcnullExpression |
|
| Pthread2CIVLTransformer |
|
| QuantifiedExpression |
A CIVL-C quantified expression, including three components, bound variable
declaration list, (optional) restriction and expression.
|
| QuantifiedExpression.Quantifier |
The different kinds of quantifiers which are possible.
|
| RealLiteralExpression |
A real literal.
|
| RecDomainLiteralExpression |
This is a rectangular domain literal expression, which is the Cartesian
product of a number of ranges, e.g.,
{range1, range2, range3, ...}.
|
| RegularRangeExpression |
Represents a CIVL-C regular range expression, which has the form
lo ..
|
| ReturnStatement |
A return statement.
|
| Scope |
A scope.
|
| ScopeofExpression |
A scopeof expression is "$scopeof(expr)".
|
| SelfExpression |
Self expression.
|
| SelfReference |
This represents the complete reference to a variable.
|
| Semantics |
Entry point of the module civl.semantics.
|
| ShortCircuitTransformer |
|
| Singleton<T> |
|
| SizeofExpression |
An expression of the form "sizeof(e)" where e is an expression.
|
| SizeofTypeExpression |
An expression of the form "sizeof(t)" where t is a type.
|
| Slice |
|
| Sourceable |
|
| StackEntry |
An entry on a call stack of a process; also known as an "activation frame".
|
| State |
A State represents the (global) state of a CIVL Model.
|
| StateFactory |
The state factory is used to create all state objects.
|
| Statement |
The parent of all statements.
|
| Statement.StatementKind |
Different kinds of statements.
|
| StatenullExpression |
This class represents a $state_null constant expression.
|
| States |
Entry point for the state module: provides a static method to get a new state
factory.
|
| StateValueHelper |
This class provides a set of interfaces for help dealing with values of
$state type objects.
|
| StructOrUnionField |
A field in a struct has a name and a type.
|
| StructOrUnionFieldReference |
This represents a reference to a field of a struct/union.
|
| StructOrUnionLiteralExpression |
|
| SubscriptExpression |
a[i], where "a" is an array and "i" is an expression evaluating to an
integer.
|
| SvcompTransformer |
Transforms svcomp programs which are preprocessed by GCC
|
| SymbolicAnalyzer |
This class provides methods dealing with symbolic expressions and states,
which represent some common-used operations like obtaining a sub-array from a
given array, etc.
|
| SymbolicUtility |
A SymbolicUtility provides all the common operations of symbolic expressions.
|
| SystemFunction |
A system function is a function that is implemented in a library executor,
not in source code.
|
| SystemGuardExpression |
A system guard expression is a sudo guard expression for system function
calls.
|
| TracePlayer |
A tool to replay a trace saved by a previous CIVL session.
|
| TraceStep |
TraceStep extends TraceStepIF for CIVL models.
|
| TransformerFactory |
This class manages the set of transformations provided by CIVL.
|
| Transforms |
|
| Transition |
This represents a CIVL transition, which is deterministic and enabled at a
certain state.
|
| Transition.AtomicLockAction |
|
| Transition.TransitionKind |
|
| Transmuter |
|
| Triple<R,S,T> |
|
| TrivialPredicate |
|
| TypeEvaluation |
Represents the result of evaluating something that returns a symbolic type,
but in two parts: the (possibly) new state resulting from side-effects
arising from the evaluation, and the symbolic type resulting from the
evaluation.
|
| UnaryExpression |
A unary operation.
|
| UnaryExpression.UNARY_OPERATOR |
|
| UndefinedProcessExpression |
Self expression.
|
| UnsatisfiablePathConditionException |
Thrown when a path condition becomes unsatisfiable, typically due to a side
effect from evaluating an expression.
|
| UpdateStatement |
|
| UserInterface |
This class provides a user interface to CIVL.
|
| Utils |
|
| Utils.Color |
|
| ValueAtExpression |
The CIVL-C $value_at(state, PID, expr) expression, evaluating
the given expression expr at the given state ($state).
|
| Variable |
A static variable.
|
| VariableExpression |
A use of a variable in an expression.
|
| Verifier |
|
| WildcardExpression |
This represents the expression ..., which is used only in
contracts and stands for an expression of any type whose value is ignored.
|
| WithStatement |
|