| Interface | Description |
|---|---|
| Var |
Abstract class for Variables for level 1.
|
| Class | Description |
|---|---|
| Abstract0 |
Class of level 0 numerical abstract values.
|
| Abstract1 |
Class of level 1 numerical abstract values.
|
| Box |
Manager factory for the interval abstract domain.
|
| Coeff |
Abstract class of constant coefficients that can appear in expressions.
|
| Dimchange |
Class of dimension change specifications for level 0 objects.
|
| Dimension |
Class of dimension specifications for level 0 objects.
|
| Dimperm |
Class of dimension permutations for level 0 objects.
|
| DoubleScalar |
Class of Scalar objects backed up by a double-precision
floating-point number.
|
| Environment |
Class of environments for level 1 objects.
|
| Generator0 |
Class of geometrical features of level 0 linear abstract elements.
|
| Generator1 |
Class of geometrical features of level 1 linear abstract elements.
|
| Interval |
Class of intervals of reals, denoted by a lower and an upper
Scalar bound. |
| Lincons0 |
Class of level 0 linear constraints.
|
| Lincons1 |
Class of level 1 linear constraints.
|
| Linexpr0 |
Class of level 0 linear expressions.
|
| Linexpr1 |
Class of level 1 linear expressions.
|
| Linterm0 |
Class of terms in level 0 linear expressions and constraints.
|
| Linterm1 |
Class of terms in level 1 linear expressions and constraints.
|
| Manager |
Class of numerical abstract domain instances.
|
| MpfrScalar |
Class of Scalar objects backed up by a
Mpfr
multi-precision floating-point number. |
| MpqScalar |
Class of Scalar objects backed up by a
Mpq multi-precision
rational. |
| Octagon |
Manager factory for the octagon abstract domain.
|
| Polka |
Manager factory for the convex polyhedron abstract domain.
|
| PolkaEq |
Manager factory for the linear equalities domain.
|
| PolkaGrid | |
| PplGrid |
Manager factory for the Parma Polyhedra Library linear
congruence equalities domain.
|
| PplPoly |
Manager factory for the Parma Polyhedra Library convex polyhedra domain.
|
| Scalar |
Abstract class of coefficients that represent scalar real numbers.
|
| StringVar | |
| Tcons0 |
Class of level 0 constraints on arbitrary expressions.
|
| Tcons1 |
Class of level 1 constraints on arbitrary expressions.
|
| Test |
Simple test for the Java Apron binding.
|
| Texpr0BinNode |
Class of binary operator nodes in
Texpr0Node level 0
expression trees. |
| Texpr0CstNode |
Class of constant leaves in
Texpr0Node level 0
expression trees. |
| Texpr0DimNode |
Class of variable leaves in
Texpr0Node level 0
expression trees. |
| Texpr0Intern |
Class of level 0 expression trees in opaque Apron representation.
|
| Texpr0Node |
Class of level 0 concrete expression trees.
|
| Texpr0UnNode |
Class of unary operator nodes in
Texpr0Node level 0
expression trees. |
| Texpr1BinNode |
Class of binary operator nodes in
Texpr1Node level 1
expression trees. |
| Texpr1CstNode |
Class of constant leaves in
Texpr1Node level 1
expression trees. |
| Texpr1Intern |
Class of level 1 expression trees in opaque Apron representation.
|
| Texpr1Node |
Class of level 1 concrete expression trees.
|
| Texpr1UnNode |
Class of unary operator nodes in
Texpr1Node level 1
expression trees. |
| Texpr1VarNode |
Class of variable leaves in
Texpr1Node level 1
expression trees. |
| Exception | Description |
|---|---|
| ApronException |
Superclass of Apron-specific exceptions that can be thrown
by numerical abstract domains.
|
| NotImplementedException |
Exception thrown when calling an abstract transfer
function that is not implemented in the domain.
|
| OutOfSpaceException |
Exception thrown by an abstract transfer function when
the maximum memory consumption is exceeded.
|
| OverflowException |
Exception thrown by an abstract transfer function in
case of an arithmetic overflow.
|
| TimeoutException |
Exception thrown by an abstract transfer function when
the timeout is exceeded.
|
The binding is based on Apron 0.9.10.
To start with Apron, you should first choose a numerical abstract
domain. i.e., any subclass of Manager. For instance,
Polka corresponds to the convex polyhedra domain.
The constructor Polka.Polka(boolean) allows you to construct one
(or several, which is mainly useful in a multi-threaded application)
abstract domain instance.
Then, you need choose whether to use level 0 or level 1 operations.
In level 0 operations, abstract elements are sets of points in a
Cartesian space Z^n * R^m, and all data-structures (expressions,
constraints, etc.) consider variables as dimensions, indexed from 0.
In level 1 operations, abstract elements are sets of points in
an Environment (i.e., set of variables) and variables
are abstract Var (possibly simple strings, using
StringVar). The main advantage of level 1 is that you do not
need to bother with the mapping from program variables to dimensions in your
static analysis (which could be tricky if variables are not created and
destroyed in a last in / first out manner): the library does it for you.
Actually, the level 1 is a implemented fully in Java, on top of the
native level 0 code.
Apron checks that dimension spaces (in level 0) or
environments (in level 1) for all the arguments are compatible.
With your Manager instance, you can now create
and manipulate abstract elements using either the Abstract0
or the Abstract1 class, depending on which level you prefer.
Note that the Manager needs to be passed as first argument
of almost all functions in these classes as it points back to the
actual abstract domain implementation instance.
To apply transfer functions such as assignments or constraint addition,
you need to create extra objects to denote expressions and constraints.
Apron has linear expressions and arbitrary expression trees,
respectively Linexpr0, Linexpr1,
Texpr0Intern, Texpr1Intern,
depending on the level you chose.
Linear expressions are akin arrays but, as they are backed by native
Apron C objects, they must be accessed with a set/get paradigm.
Expression trees are a bit more complex: the internal native C
data-structures are a bit too complex to be accessed directly.
Instead, the Java binding provides pure
Java expression trees (Texpr0Node, Texpr1Node
and subclasses), and wrappers for opaque Apron C expression trees
(Texpr0Intern, Texpr1Intern).
The later are used for Abstract0 and Abstract1
arguments and return values; and can be converted to and from the former
for easier construction and inspection on the Java side.
Each expression type (linear / tree, level 0 / level 1) has a corresponding
constraint type, using the expression as left argument, 0 as right
argument, and some comparison operator (plus an optional extra number
to denote modulo).
All expressions and constraints use a generic Coeff
class to denote constants. These can be simple scalars (Scalar),
or intervals with constant scalar bounds (Interval).
Scalars can in turn be either represented by machine floating-point
numbers (DoubleScalar), arbitrary-precision fractions
(MpqScalar), or arbitrary-precision floating-point
numbers (MpfrScalar).
You can choose whichever suites you to talk to Apron and, when Apron
gives you back some Scalar, you can convert it back
to a double, a Mpq, or a Mpfr.
Remember that abstract operations may be inexact and imprecise. The contract states that abstract domain implementations can perform approximations but must always respect soundness: a result abstract element or interval may be an over-approximation. Likewise, a predicate is definitely true if the function returns true, but is unknown if the function returns false.
The Apron library changes the FPU rounding-mode towards +oo, to ensure
the soundness of all computations.
This can confuse some JVMs.
For instance, this causes an error on Sun's JDK 1.6 when the option
-Xcheck:jni is used.