Previous: Functionalities of the interface at level 0, Up: APRON Rationale and Functionalities
Functionalities of the interface at level 1 ¶
We focus on the changes brought by the level 1 w.r.t. the level 0.
Next: Semantics and Representation of an abstract value, Previous: Functionalities of the interface at level 1, Up: Functionalities of the interface at level 1
Variables ¶
Dimensions are replaced by variables.
In the C interface, variables are defined by a generic type
(char*, structured type, ...), equipped with the operations
compare, copy, free, to_string. In the
OCAML, for technical reasons, the type is just the string
type.
Environments manages the correspondance between the numerical
dimensions of level 0 and the variables of level 1.
Next: Operations on environments, Previous: Variables and Environments, Up: Functionalities of the interface at level 1
Semantics and Representation of an abstract value ¶
The semantics of an abstract value is a subset
X -> (N+R).
where X is a set of variables.
Abstract values are typed according to their environment.
It is represented by a structure
struct ap_abstract1_t {
ap_abstract0_t *abstract0;
ap_environment_t *env;
};
Other datatypes of level 0 are extend in the same way. For instance,
struct ap_linexpr1_t {
ap_linexpr0_t *linexpr0;
ap_environment_t *env;
};
Next: Dynamic typing w.r.t. environments, Previous: Semantics and Representation of an abstract value, Up: Functionalities of the interface at level 1
Operations on environments ¶
- creation, merging, destruction
- addition/removal/renaming of variables
Next: Operations on variables in abstract values, Previous: Operations on environments, Up: Functionalities of the interface at level 1
Dynamic typing w.r.t. environments ¶
For binary operations on abstract values, the environments should be
the same.
For operations involving an abstract value and an other datatype
(expression, constraint, ...), one checks that the environment of
the expression is a subenvironment of the environment of the abstract
value, and one resize if necessary.
Previous: Dynamic typing w.r.t. environments, Up: Functionalities of the interface at level 1
Operations on variables in abstract values ¶
Operations on dimensions are lifted to operations on variables:
- Projection/Elimination of one or several variables with constant
environment;
- Addition/Removal/Renaming of variables with corresponding change
of environment;
- Change of environment (possibly combining removal and addition of variables);
- Expansion and folding of variables.