All Classes and Interfaces
Class
Description
An abstract function is an uninterpreted mathematical function.
An expression representing a call of an abstract function.
An accuracy assumption builder provides logic for determining additional
assumptions that should be added after an assumption involving an abstract
function call.
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.Entry point of the module civl.analysis.
This represents a predicate in CNF, containing a number of predicates, called
clauses, i.e., p1 & p2 & ...
This interface provides methods for dealing with array slices, e.g.
A CIVL-C quantified expression, including three components, bound variable
declaration list, (optional) restriction and expression.
This class provides methods for reshaping arrays.
This represents the reference to an array, which could be:
element
wildcard
range
This interface provides a collection of methods that manipulating symbolic
expressions whose symbolic type has ARRAY kind.
The data structure for describing array shapes, including dimensions,
extent for each dimension and slice size for each sub-array with lower
dimension.
the data structure for describing array slices.
An assignment statement.
This represents an atomic execution step, which represents the execution of
exactly one transition.
A binary operation.
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); A literal boolean value.
A bound variable is a variable used in a quantified expression.
This represents a function call event of a
depends clause.A function call or spawn.
A cast of an expression to a different type.
The main CIVL class, containing the main method, which provides the command
line interface for using CIVL.
The type for an array of T.
The type for an array of T where the extent is specified.
A CIVLConfiguration object encompasses all the parameters used to configure
CIVL for the execution of one or more tasks.
This class manages all constant configurations of the system.
Kinds of deadlock: absolute, potential or none.
Error state equivalence semantics for suppressing logging of redundant
errors.
The different MPI implementation model that CIVL provides.
This is the only one CIVLDomainType associated to the $domain type in
program.
An enumeration type.
CIVLErrorLogger logs all errors of the system.
Root of CIVL exception hierarchy, representing any kind of event where
something goes wrong in CIVL.
A certainty level gages how certain we are that this is error is a real
error, i.e., not just a spurious error.
This represents an error during the execution of a program.
A CIVL function.
Extends an execution exception with a state at which error occurred.
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.
This represents an entry in the error log of CIVL.
A
CIVLType representing a set of memory locations.Implementations of
CIVLMemType.MemoryLocationReference represent references
to a subset of a value of a variable/heap objectThis represents the first part of a $parfor construct, i.e., spawning
processes according the specified domain.
Type of a pointer.
A primitive type is a type of which there is only one instance.
Enum class for representing different properties that CIVL checks for.
The $scope type in the CIVL-C language.
A
CIVLType representing a set of a non-set kind CIVLType.A CIVLSource object represents a range of text in a source file.
Extends an execution exception with a state at which error occurred.
StateManager extends
StateManager for CIVL models.Represents a "record" type (i.e.
An exception thrown when there is syntax error in the program being verified,
e.g., calling $choose_int with more than one arguments, etc.
Parent of all types.
The CIVL type factory provides the CIVL primitive types, like
$bool, int, float, $scope
, etc.An exception thrown when there is not necessarily anything wrong with the
program begin verified, but some CIVL feature has not yet been implemented.
This represents a code analyzer for analyzing source code for a certain
property.
A command line represents the command line information for running CIVL.
CIVL command line kinds: normal, or compare.
This contains the names of all commands supported by CIVL, either it is a
normal command or a compare command.
This represents a composite event, which could be a
union/difference/intersect of another two depends events.
The ternary conditional expression ("?" in C).
This factory is to create new instances of function contract components.
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).
This represents an event which is used as one argument of the
depends clause.An uninterpreted call to the derivative of an abstract function.
This expression encodes the claim that a real, abstract function is
differentiable.
This transformer instruments the model so as to direct
the symbolic execution down a subset of program paths.
This is the guard expression of CIVL for loops (
$for).
Updates the loop variables with the next element of a domain.
This analysis uses an iterative fixed-point
data flow framework to find the dominators of
any node in a graph.
A dot expression is a reference to a field in a struct or union.
This class is a immutable data structure that stores a set of memory
locations.
Entry point of the module dynamic.
A DynamicScope is a runtime instance of a static scope.
A "DynamicTypeOf" expression.
Enabler extends
EnablerIF for CIVL models.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.
This is the CIVL main evaluator.
The parent of all expressions.
The representation for the "fold expression" in ACSL, e.g.
A fragment is a sequence of statements.
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.
This represents a non-named behavior of the ACSL function contract.
This represents a block of ACSL contract for a function.
ContractKind: This kind is used to denotes all kinds of contracts.
A function guard expression is the guard expression of a function
call with a function pointer.
An identifier.
An expression yielding the initial value of a variable.
An integer literal.
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
The IO transformer transforms
all function calls printf(...) into frpintf(stdout, ...) all function calls scanf(...) into fscanf(stdin, ...) all function calls fopen(...) into $fopen(...)
all function calls printf(...) into frpintf(stdout, ...) all function calls scanf(...) into fscanf(stdin, ...) all function calls fopen(...) into $fopen(...)
This is the entry point of the module kripke.
A CIVL-C quanti, bound variable declaration list, (optional) restriction and
expression.
A left-hand-side expression.
A Library Enabler provides a method to compute the enabled transitions of
system function calls at a certain state for a give process.
The library enabler loader provides the mechanism for loading the library
enabler of a certain library.
A Library Evaluator provides a method to "evaluate" the guard of each system
function call.
The library evaluator loader provides the mechanism for loading the library
evaluator of a certain library.
A Library Executor provides the semantics for system functions defined in a
library.
The library executor loader provides the mechanism for loading the library
executor of a certain library.
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.
The parent of all literal expressions.
The parent of all locations.
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.
A logic function is a function whose definition (body) is either absent (i.e.
This class represents a group of loop annotations for a loop, including loop
invariants, loop assigns and loop variants.
A statement for dynamic allocation of objects.
This represents a
\read or \write event of a
depends clause.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.
A memory unit expression is an expression that represents (part of) the
memory related to some variable.
A memory unit set represents a set of memory units.
A model of a CIVL program.
Class to provide translation from an AST to a model.
This file contains the constants used by the model builder/translator, which
reflects the translation strategy of CIVL.
The factory to create all model components.
This is the entry point of the module model.
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 transforms an AST of an MPI program into an AST of an
equivalent CIVL-C program.
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.
A named behavior contains a name and assumptions in addition to those
components contained by
FunctionBehavior.Marker interface for a noop statement.
OpenMP2CIVLTransformer transforms an AST of an OpenMP program into an AST of
an equivalent CIVL-C program.
This transformer analyzes OpenMP constructs and converts them to simpler,
i.e., less concurrent, instances of constructs.
Base class for various tools that require executing a CIVL model.
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
An object supporting a "print" method.
A ProcessState represents the state of a process (thread of execution) in a
CIVL model.
A CIVL-C quantified expression, including three components, bound variable
declaration list, (optional) restriction and expression.
The different kinds of quantifiers which are possible.
A real literal.
This is a rectangular domain literal expression, which is the Cartesian
product of a number of ranges, e.g.,
{range1, range2, range3, ...}.Represents a CIVL-C regular range expression, which has the form
lo ..A return statement.
A scope.
A scopeof expression is "$scopeof(expr)".
Self expression.
This represents the complete reference to a variable.
Entry point of the module civl.semantics.
A
SeqSet represents a set of sequences of nonnegative integers.An expression of the form "sizeof(e)" where e is an expression.
An expression of the form "sizeof(t)" where t is a type.
An entry on a call stack of a process; also known as an "activation frame".
A State represents the (global) state of a CIVL Model.
The state factory is used to create all state objects.
The parent of all statements.
Different kinds of statements.
This class represents a $state_null constant expression.
Entry point for the state module: provides a static method to get a new state
factory.
This class provides a set of interfaces for help dealing with values of
$state type objects.
A field in a struct has a name and a type.
This represents a reference to a field of a struct/union.
a[i], where "a" is an array and "i" is an expression evaluating to an
integer.
Transforms svcomp programs which are preprocessed by GCC
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.
A SymbolicUtility provides all the common operations of symbolic expressions.
A system function is a function that is implemented in a library executor,
not in source code.
A system guard expression is a pseudo guard expression for system function
calls.
A tool to replay a trace saved by a previous CIVL session.
TraceStep extends
TraceStepIF for CIVL models.This class manages the set of transformations provided by CIVL.
This represents a CIVL transition, which is deterministic and enabled at a
certain state.
This represents a CIVL transition, which is deterministic and enabled at a
certain state.
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.
A unary operation.
Self expression.
Thrown when a path condition becomes unsatisfiable, typically due to a side
effect from evaluating an expression.
This class provides a user interface to CIVL.
The CIVL-C
$value_at(state, PID, expr) expression, evaluating
the given expression expr at the given state ($state).A static variable.
A use of a variable in an expression.
This represents the expression
..., which is used only in
contracts and stands for an expression of any type whose value is ignored.