[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
At the level 0 of the interface, an abstract value is a structure @verbatim struct ap_abstract0_t { ap_manager_t *manager; /* Explicit context */ void *value; /* Abstract value representation (only known by the underlying library) */ } The context is allocated by the underlying library, and contains an array of function pointers pointing to the function of the underlying library. Hence, it indicates the effective type of an abstract value.
The validity of the arguments of the functions called through the
interface is checked before the call to effective functions. In case
of problem, an invalid_argument
exception is raised.
The semantics of an abstract value is a subset
X of N^p x R^q
Abstract values are typed according to their dimensionality (p,q).
Taking into account or not the fact that some dimensions are integers is left to underlying libraries. Treating them as real is still a correct approximation. The behaviour of the libraries in this regard may also depend on some options.
In addition to abstract values, the interface also manipulates the following main datatypes:
double
.
double
, the IEEE754 is assumed and the corresponding standard representation is used.
X = { lambda0 p0 +...+ lambdaM pM + mu0 r0 +...+ muN rN | lambda0 +...+ lambdaN = 1 and forall J : muJ >= 0 }The APRON datatype for generators distinguishes points (sum of coefficients equal to one), rays (positive coefficients), lines (or bidirectional rays, with unconstrainted coefficients), integer rays (integer positive coefficients) and integer lines (integer coefficients).
We identified several notions:
There are two printing operations:
The printing format is library dependent. However, the conversion of abstract values to constraints (see below) allows a form of standardized printing for abstract values.
Serialization and deserialization of abstract values to a memory buffer is offered. It is entirely managed by the underlying library. In particular, it is up to it to check that a value read from the memory buffer has the right format and has not been written by a different library.
Serialization is done to a memory buffer instead of to a file descriptor because this mechanism is more general and is needed for interfacing with languages like OCAML.
Four basic constructors are offered:
Predicates are offered for testing
Some properties may be inferred given an abstract values:
Notice that the second operation implements linear programming if it is exact. The third operation is not minimal, as it can be implemented using the first one, but it was convenient to include it. But the fourth operation is minimal and cannot be implemented using the second one, as the number of linear expression is infinite.
Parallel assignement and substitution ar enot minimal operations, but for some abstract domains implementing them directly results in more efficient or more precise operations.
Widening, either simple or with threshold, is offered. A generic widening with threshold function is offered in the interface.
Topological closure (i.e., relaxation of strict inequalities) is offered.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |