All Classes and Interfaces
Class
Description
The root of the ABC non-runtime-exception hierarchy.
The root of the ABC runtime exception hierarchy.
An error which is thrown when there is feature that has not yet been
implemented in ABC.
An abstract function definition contains the information for an abstract
function (i.e.
This class is the representation of abstract values.
A value of the form "&(lhs)", where lhs is a left hand side expression.
The
_Alignof(typename) operator.This represents an ACSL allocation clause, which has the syntax
or
allocates p1, p2, p3; or
frees p1, p2, p3;Simple factory class providing static methods for creating new instances of
Analyzer.An analyzer is an object which performs some kind of analysis on an AST,
typically leaving behind the information in the AST.
This represents ACSL-CIVLC
\anyact action to be used in
depends contract clauses.Represents a conversion from any arithmetic type to another arithmetic type
(not just the "usual arithmetic conversions").
The arithmetic types are "char", the signed and unsigned integer types,
enumeration types, and the floating types (which include the real and the
complex floating types).
An implicit conversion from array type to pointer type.
An array designator specifies the index of an element of an array being
initialized.
A CIVL-C array lambda expression, including three components, bound variable
declaration list, (optional) restriction and expression.
Represents an array type.
Represents an array type.
An expression in which the operator is the C
-> (arrow)
operator.
An instance of this class represents an abstract object.
An abstract representation of one of the following assignments:
BASE: U = &U
SIMPLE: U = U
COMPLEX_LD: *U = U
COMPLEX_RD: U = *U
where U is a
AssignExpIF which represents an abstract object.
BASE: p = &a
SIMPLE: p = a
COMPLEX_LD: *p = a
COMPLEX_RD: p = *a
This class represents an integral parameter "c|*" of an abstract object that
has the form of
U + (c|*) or U[c|*].An ACSL
assigns or ACSL-CIVLC reads clause
specifies a set of existing memory units.This represents an ACSL
assumes clause, which has the following
syntax:
A representation of a program as an abstract syntax tree.
An object which translates an ANTLR tree to an ABC AST.
Runtime exception thrown when something goes wrong with the AST.
An ASTFactory is used to create all objects associated to an AST.
Root of the AST node type hierarchy.
The different kind of AST nodes.
Factory class providing static method to produce a new
ASTFactory.An atomic node represents a CIVL-C
$atomic statement.
An atomic type, specified by
_Atomic ( type-name ) or by using
the _Atomic type qualifier.An atomic type, specified by "_Atomic ( type-name )".
A key to be used as a key-attribute pair.
A very basic partial implementation of
Transformer.A behavior is an entity which has a name and an associating behavior node.
This represents a named behavior of the ACSL specification.
An item that can appear in a "block".
An event that represents a function call with certain arguments, which is a
kind of Depends Event.
A C cast expression has the form
(typeName)expr.A value obtained by casting a value to a new type.
An instance of this interface represents a single Unicode character occurring
as a literal element in a C program.
A character token represents a character constant in a source program, e.g.,
'a'.A "choose" statement has the form "choose { s1 ...
A post-preprocessor token.
This class exports the constants for token types from CivlCParser.
Represents a finite sequence of
CivlcToken.
Extends ANTLR's
TokenSource interface by adding some additional
functionality: getting the macro information, and methods to get the number
of tokens produced so far and to retrieve any token produced so far by index.
Represents a CIVL
$for or $parfor statement.A simple, generic implementation of
Entity.An implicit conversion from one pointer type to another pointer type in the
case where either the two types are compatible or the second type is obtained
by adding a qualifier to the type of thing pointed to.
Conversion from one structure or union type to a compatible version of that
type.
This represents the completeness clause of ACSL, which could be either
complete or disjointAn composite event
The operator of a composite event
A compound initializer (written with curly braces in C) is used to initialize
an array, struct, or union.
Compound literals are used to represent literal array, structure, and union
values.
A compound literal is an abstract representation of a literal array, struct,
or union value in a C program.
A compound statement is a sequence of statements and declarations within
curly braces: "{ ...
A
Concatenation represents the concatenation of a sequence of tokens.Configuration constants.
The different machine architectures that can be used to specialize
translation and analysis.
The language of the program being processed.
A "constant" in the sense of the C11 Standard.
A contract node represents an element that may occur in a procedure contract.
The kinds of contract nodes
A conversion is an implicit operation that may change a value and/or the type
of the value.
Kind of conversions
A factory for producing instances of
Conversion.Factory class providing static method to produce a
ConversionFactory.A list of variable declarations, such as might occur as an initializer in a
for loop.
The root of the declaration node type hierarchy.
This represents an event of the
depends clause.A
depends clause specifies part of the dependence relation used
in partial order reduction (POR).A CIVL-C derivative expression is a function call to the partial derivative
of an abstract function.
A designation node specifies a sequence of designators.
A designator is used in a compound initializer to specify a part of a
compound structure.
The CIVL-C type
$domain or $domain(n).Represents use of the CIVL-C domain type, either "$domain" alone, or one of
the sub-types "$domain(n)" for some positive integer constant n.
A C expression in which the operator is the
. (dot) operator,
used to specify a member of a structure or union.An "ensures" clause in a procedure contract represents a post-condition.
Factory class providing a static method to get a new
EntityFactory.
An entity is an underlying program "conceptual thing" that can be named by an
identifier.
The different kinds of Entity.
A factory for producing instances of
Entity, and some related utility
methods.An enumeration constant node represents a use of an enumeration constant as
an expression.
An enumeration type.
An enumeration type.
An Enumerator corresponds to one of the identifiers in the list in an
enumeration.
The declaration of an enumerator (enumeration constant) within an enumeration
type definition.
A node representing any kind of C expression.
An enumerated type used to categorize the different kinds of expression
nodes.
This represents an ACSL extended quantification expression.
A Field is a member of a structure or union.
Represents a declaration of a field (member) in a struct or union type.
A field designator is used in an initializer for a struct or union.
A
FileIndexer keeps track of all source files opened during an
invocation of ABC.A floating constant node represents an occurrence of a literal floating point
number in a program.
The floating types come in four kinds:
float,
double, long double, representing increasing
precision, and "real", a CIVL-C type denoted $real representing
the mathematical real numbers.A flow-insensitive PointsToAnalyzer takes a program (
AST), builds
points-to graph for the program and provides service for querying the "may
points-to" set of a lvalue
A marker interface indicating this construct can be used as the first clause
in a
for loop.A for loop, in addition to the expression and body that all loops possess,
has an initializer and incrementer.
A formation is a record of the history of events that went into the formation
of a token.
Entry point of the front module.
A function is an entity which takes inputs, executes a statement, and
possibly returns a result.
Node representing a function call.
An implicit conversion of a function type T to the type pointer-to-T.
A node representing a function declaration.
Represents a function definition, i.e., a function declaration which includes
the function body.
A FunctionMacro represents a C preprocessor function-like macro, which has
the from
#define f(X1,X2,...) ....According to C11, a function type is characterized by the return type and the
number and types of the arguments.
Represents the association between a type and an expression for use in a
generic selection expression.
Represents a C11 generic selection construct; see C11 Section 6.5.1.1.
Represents a C "goto labelName;" statement.
This represents a
guards clause that specifies a guard for a
function.A node representing one of the two CIVL-C constant expressions of type
$scope: $here (the dynamic scope in which the
expression is evaluated), or $root (representing the root
dynamic scope).Represents the use of an identifier as an expression.
An identifier can denote: (1) an object, (2) a function, (3) a tag of a
structure, union, or enumeration, (4) a member of a structure, union, or
enumeration, (5) a typedef name, or (6) a label name.
An Inclusion represents the application of a preprocessor
#include directive.
A marker interface for any node that can be used as an initializer.
The flow-insensitive abstraction of a function body for points-to analysis.
some sv-comp examples are using conversions between pointers and integers.
An integer constant node represents the occurrence of a literal integer
constant in a program.
Marker interface for all "integer type" nodes.
The invocation graph node is described in detail in paper "Context-sensitive
inter-procedural points-to analysis in the presence of function pointers"
Details these kinds can be found in paper "Context-sensitive
inter-procedural points-to analysis in the presence of function
pointers".
creating invocation graph nodes
A label followed by a colon may precede a statement in a C program.
Represents a label in a program.
A lambda function, including two/three components, a bound variable
declaration (optional) and the lambda term.
A lambda type represents the type of an lambda expression (see
LambdaNode .A
TypeNode representing a $lambda(free-var-type:func-type) typeA literal object is either a
ScalarLiteralObject or a
CompoundLiteralObject.Root of type hierarchy for every kind of loop statement.
An Lvalue conversion, i.e., a conversion from the type of an lvalue to the
type of the value obtained by evaluating that lvalue.
An abstract representation of a preprocessor macro.
The body of a
Macro definition consists of a sequence of
Macro.ReplacementUnits, each of which comprises a preprocessing token
(a non-whitespace token known as the "replacement token" in C11) plus
some possible whitespace.A MacroExpansion represents an instance of the expansion of a preprocessor
(object or function) macro, which replaces one token by a sequence of new
tokens.
A MemConversion converts an expression of pointer or set-of pointer type to
$mem type.
A depends event which specifies reading or writing a list of memory units.
This class represents the
$mem type which stands for a set of
(typed) memory locations.An contract block introduced by the
mpi_collective(MPI_Comm, Kind): contract constructor.
This
ContractNode represents an "mpi event", which represents a set
of specific actions that a process performs during runtime.
The kinds of the events.
This
MPIContractExpressionNode denotes an MPI absent expression, which
states a path predicate for an MPI collective-style function.This represents the no-act event
\noact, which is an event of
depends clauses.
The factory used to construct the nodes of Abstract Syntax Trees.
A factory class providing a static method to produce a new
NodeFactory.Constant
$nothing, argument of $assigns / $reads
contract clauses.Conversion of a null pointer constant to any pointer type.
A null statement: ";".
An Object macro represents a C preprocessor object macro: a directive of the
form
#define X ... where X is the name of the macro
and the ... is a list of replacement tokens.This represents a
$object_of of $region_of
expression.A type of a
Variable, also known as an "object" in C.This represents an OpenMP atomic construct, which has the syntax:
This represents an OpenMP declarative directive, which can only be placed in
a declarative context.
The kind of an OpenMP declarative pragma.
Represents an OpenMP executable Construct.
The children of an OmpExecutableNode are: SequenceNode<IdentifierExpressionNode> "sharedList", the list of identifiers declared by
The children of an OmpExecutableNode are: SequenceNode<IdentifierExpressionNode> "sharedList", the list of identifiers declared by
shared
SequenceNode<IdentifierExpressionNode> "privateList", the list of
identifiers declared by private
SequenceNode<IdentifierExpressionNode> "firstprivateList", the list
of identifiers declared by firstprivate
SequenceNode<IdentifierExpressionNode> "lastprivateList", the list
of identifiers declared by lastprivate
SequenceNode<IdentifierExpressionNode> "copyinList", the list of
identifiers declared by copyin
SequenceNode<IdentifierExpressionNode> "copyprivateList", the list
of identifiers declared by copyprivate
SequenceNode<OmpReductionNode> "reductionList", the list of
operators and identifiers declared by reduction
StatementNode, the statement node affected by this pragma.The kind of this OpenMP statement:
PARALLEL: the parallel construct
SYNCHRONIZATION: synchronization constructs such as master, critical,
barrier, taskwait, taskgroup, atomic, flush, ordered, etc.
WORKSHARING: worksharing constructs such as sections (section) and
single.
SIMD: simd directive, objects of this kind are instances of
OmpSimdNode
This interface represents the OpenMP loop construct.
The schedule kind of an OpenMP for pragma.
This represents an OpenMP reduction identifier.
A node representing any kind of an OpenMP pragma.
The kind of this OpenMP pragma.
This represents an OpenMP parallel pragma.
This represents an OpenMP reduction clause.
The kind of this reduction clause, either
OPERATOR if the reduction-identifier is one of the following:+, -, *, &,
|, ^, &&, ||, min and max; or
FUNCTION if the reduction-identifier is an identifier except "min" and
"max" (ignoring the letter case for these two strings).
The kind of this reduction operator, all (SUM, MINUS, MULTIPLY, MAX, MINBAND,
BOR, BXOR, LAND, LOR, UDEF) except for "UDEF" are OpenMP built-in operators
according to OpenMP Standard ver.4.5
(https://www.openmp.org/wp-content/uploads/openmp-4.5.pdf).
A simd directive, which may have the following clauses:
if([simd :]scalar-logical-expression)
safelen(length)
simdlen(length)
linear(list[ : linear-step])
aligned(list[ : alignment])
nontemporal(list)
private(list)
lastprivate([ lastprivate-modifier:] list)
reduction([ reduction-modifier,]reduction-identifier : list)
collapse(n)
order(concurrent)
This represents an OpenMP reduction clause with the reduction operator being
one of the following operators:
For C:
For Fortran: (NOT case sensitive)
For C:
max,min,+,-,*,
&,|,^,&&, and
|| For Fortran: (NOT case sensitive)
MAX,MIN,+,-,*,
IAND,IOR,IEOR,.AND.,
.OR., .EQV. and .NEQV.This interface stands for synchronization constructs of OpenMP, including:
master
critical
barrier
flush
atomic
Currently, taskwait and atomic constructs are not supported.
The kind of this OmpSyncNode:
MASTER: the master construct
CRITICAL: the critical construct
BARRIER: the barrier construct
FLUSH: the flush construct
ORDERED: the ordered construct
This represents an OpenMP worksharing construct, either a loop,
sections/section, or single construct.
The kind of this OmpWorksharingNode:
FOR: the loop construct
SECTIONS: the sections construct
SECTION: the section construct
SINGLE: the single construct
A node that represents an expression built using an operator.
An enumerated type for all the different operators that can occur in an
OperatorNode.
A declaration of a variable or function via a C "declarator".
The different kinds of ordinary declarations.
Represents an ordinary label (i.e., a label which is not a
case
or default label).A node with two children, the first of type S and the second of type T.
A
Parser is used to parse a CivlcTokenSource --- a stream of
CivlcTokens --- and create a ParseTree.This represents a parse tree which is the result of preprocessing and parsing
a source in various languages, such as CIVL-C, Fortran, C, etc.
some sv-comp examples are using conversions between pointers and integers.
Any pointer type can be explicitly cast to the boolean type: if the pointer
is NULL, it maps to the boolean value
false, else it maps to
true.
A points-to graph G is a tuple (V, E, pt) where V are nodes, E are edges and
pt is a function from V to sets of V.
A Converter rephrases a token stream output from a C Preprocessor.
A pragma may be included in the AST wherever a statement or an external
definition may occur.
The ACSL predicate node, which in the view of ABC, is just a function with a
boolean return type.
A Preprocessor is used to preprocess source files.
An exception that is thrown when there is a problem evaluating a preprocessor
expression.
Represents the CIVL-C null process constant
$proc_null, which is
a constant of type $proc.
An abstract representation of a program.
The different kinds of linkage an entity may have: external, internal, or
none.
This factory is used to produce a whole
Program from a set of ASTs
representing individual translation units.A CIVL-C quantified expression, including three components, bound variable
declaration list, (optional) restriction and expression.
An enumerated type for the different quantifiers.
Represents a CIVL-C regular range expression, which has the form
lo ..Converts a regular range to a (one-dimension) domain.
A CIVL-C remote expression is used to reference a variable in another
process.
A
requires clause in a CIVL-C procedure contract.Represents the CIVL-C built-in variable
$result, which
represents the value returned by a function.Represents a CIVL-C
$run expression, which has the form
$run statement.The statement s can be any single
StatementNode or a CompoundStatementNode which is wrapped by
a pair of curly braces.A scalar literal object is defined by an ordinary expression that occurs
within a compound initializer.
A lexical (static) scope in a translation unit.
The different kinds of scopes: file, block, function, function-prototype,
and contract.
Represents a CIVL-C scope-of expression, which has the form
$scopeof(lhs), where lhs is a left-hand-side
expression.
A CIVL-C scope-parameterized declaration node.
Represents the CIVL-C built-in variable
$self, which has type
$scope and evaluates to the dynamic scope in which the variable
is being evaluated.A node in which all children have type
T.
A set type is the type for expressions that represent sets of objects.
Represents a C "signed or unsigned integer type."
The interface for create a points-to analyzer
Simple implementation of Iterator for iterating over a sequence consisting of
a single element.
An interface indicating that this object can be used as an argument to the C
sizeof operator.Represents a C
sizeof(...) expression.A "Source" represents a range of CTokens (post-preprocessor tokens) from the
token stream that forms the input to the parser.
Information object for a source file processed by ABC.
Represents a CIVL-C
$spawn expression, which has the form
$spawn f(e1,...,en).An instance of this class represents a "standard basic type".
The 5 "standard" signed integer types.
The 5 kinds of standard signed integer types.
The class collects together the standard type definitions, e.g., size_t,
ptrdiff_t, etc.
This represents a GNU C statement expression.
Represents the CIVL-C null state constant
$state_null, which is
a constant of type $state.A static assertion has syntax
_Static_assert ( constant-expression , string-literal ).Represents use of the '#' operator in a function-like macro application.
A string literal object results from processing a string literal in the
source code.
The different kinds of strings, based on the kind of characters they
contain.
Represents an occurrence of a string literal in a program, which is a string
surrounded by double quotes.
A StringToken is formed from a sequence of one or more CTokens.
A structure or union type.
Represents a label in a
switch statement of the form
case constant-expression: or default:.Represents a C
switch statement.Marker interfaces for
StructureOrUnion and Enumeration
entities.An object used to print how long it takes to do things.
A factory for producing all the objects under the control of the token
module.
This class is the entry point for the "token" module.
Utility class providing static methods dealing with Token objects.
This class manages the set of transformations provided by an execution of
ABC.
A
Transformer is a tool used to transform an AST in some way,
or, more precisely, it provides a method Transformer.transform(AST) which takes
an AST and returns the transformed AST.Represents the formation of new tokens by a transformer.
An instance of Type represents a C type.
The different kinds of types.
An abstract representation of a
typedef construct: binds a name
to a type.A node representing a typedef declaration.
A factory for producing C types, which are represented as instances of
Type.The different kinds of type nodes.
GNU C language reference 6.6 Referring to a Type with typeof
Another way to refer to the type of an expression is with typeof.
A value which is a function of a type, such as "sizeof(type)" or
"_Alignof(type)".
An unqualified object type is an object type without any qualifier (const,
volatile, etc.).
An exception for which the source (in the source program being compiled) is
unknown.
This node represents an expression
$update($collator c) f().The CIVL-C
$value_at(state, PID, expr) expression, evaluating
the given expression expr at the given state ($state).Constant expressions are discussed in C11 Sec.
A variable ("object") entity.
An enumerated type for the four different kinds of "storage duration"
defined in the C11 Standard.
A declaration of a variable ("object").
A conversion between the type pointer-to-void and a pointer to an object
type.
Represents a CIVL-C guarded command.
Syntax