-
Notifications
You must be signed in to change notification settings - Fork 35
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit d1ce5b1
Showing
328 changed files
with
113,536 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
|
||
The APRON interface has been designed by the research teams involved in the | ||
APRON project (http://www.cri.ensmp.fr/apron/). | ||
|
||
The related software developpements have been conducted by the following | ||
people: | ||
|
||
Bertrand Jeannet Main author of num, mlgmpidl, apron, mlapronidl, | ||
and newpolka packages. | ||
|
||
Sebastian Pop Adaptation of the Omega library (to come). | ||
|
||
Antoine Mine Author of the Octagon Abstract Domain Library and its | ||
adaptation to APRON interface. | ||
Binding to the Parma Polyhedra Library. | ||
Author of num package. |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,249 @@ | ||
Version 0.9.10 | ||
|
||
- Migration advices (due to some API and compilation process changes) | ||
|
||
* C API: | ||
� ap_pkgrid_manager_alloc has a new signature | ||
|
||
* OCaml API: | ||
� PolkaGrid.manager_alloc_(loose|strict) are replaced by | ||
PolkaGrid.manager_alloc with a new signature. | ||
|
||
* OCaml compilation and Makefiles | ||
� Typical commands | ||
|
||
ocamlc -o mlexample.byte | ||
bigarray.cma gmp.cma apron.cma box.cma -cclib "-lboxMPQ" mlexample.ml | ||
ocamlopt -o mlexample.opt | ||
bigarray.cmxa gmp.cmxa apron.cmxa box.cmxa -cclib "-lboxMPQ" mlexample.ml | ||
are replaced by | ||
|
||
ocamlc -o mlexample.byte | ||
bigarray.cma gmp.cma apron.cma boxMPQ.cma mlexample.ml | ||
ocamlopt -o mlexample.opt | ||
bigarray.cmxa gmp.cmxa apron.cmxa boxMPQ.cmxa mlexample.ml | ||
|
||
- Compilation and linking process | ||
|
||
* Support for dynamic libraries added (new HAS_SHARED flag in | ||
Makefile.config) | ||
|
||
* IMPORTANT CHANGE for OCaml compilation: | ||
(see migration advices) | ||
|
||
- OCaml library files box.cma, polka.cma become now | ||
boxMPQ.cma, boxRll.cma, polkaRll.cma, etc... | ||
|
||
� No need any more to use the -cclib option to choose the | ||
underlying number representation. | ||
|
||
� Former box.cma, oct.cma, polka.cma are soft links to MPQ | ||
versions (for compatibility | ||
|
||
- Use of dynamic libraries when possible, with -dllib feature of | ||
ocamlc for bytecode executables. | ||
|
||
� No need for custom bytecode interpreter and toplevel | ||
� Enable the use of pretty-printer depending on C code in ocamldebug | ||
|
||
- API | ||
|
||
* Better (correct) signature for Abstract0.permute_dimensions: | ||
old: permute_dimensions : 'a Manager.t -> 'a t -> Dim.perm option -> 'a t | ||
new: permute_dimensions : 'a Manager.t -> 'a t -> Dim.perm -> 'a t | ||
|
||
* pkgrid/PolkaGrid product library: new signature for the manager | ||
allocation function | ||
|
||
* New ap_dimchange2_t datatype, for specifying addition followed by removal | ||
of dimensions. Generated by ap_environment_dimchange2 function and used by | ||
ap_abstract0_apply_dimchange2 function. | ||
|
||
* Octagon domain now supports hashing | ||
|
||
* Newpolka library: real canonical form for strict polyhedra, compatible | ||
with the hash function. | ||
|
||
* OCaml API for domains (box,oct,polka,ppl,polkaGrid): | ||
new functions allowing type conversion (for instance between | ||
Oct.t Apron.Manager.t and 'a Apron.Manager.t). | ||
|
||
- Bugs corrected: several | ||
|
||
- Distribution/Packaging | ||
|
||
* Optional interface to PPL upgraded to 0.10 (but still support only | ||
polyhedra and linear congruences). No need with version 0.10 to apply a | ||
patch (see ppl/README for more details. | ||
|
||
- Internal API | ||
|
||
* Change of signature for itv_join (now requires itv_internal_t* object); | ||
|
||
Version 0.9.9: | ||
|
||
- API: | ||
|
||
* Important change: tbool_t replaced by bool in tests in flags | ||
exact and best (C modules ap_abstractX and ap_manager, OCaml | ||
modules AbstractX and Manager) | ||
|
||
In source code, | ||
* tbool_top,tbool_false should be replaced by false, | ||
* f(...)==tbool_true by f(...) | ||
* f(...)!=tbool_true by !f(...) | ||
|
||
* MPFR numbers added as possible numerical types (besides GMP | ||
MPQ and C double) | ||
|
||
* hash functions added in most places: | ||
* bound_hash, itv_hash, linexpr0_hash, texpr0_hash, | ||
ap_abstract0_hash, ap_abstract1_hash, ap_environment_hash, | ||
ap_var_hash | ||
* in libraries, hash implemented for itv and newpolka | ||
(for others, raises not implemented). | ||
* in OCaml API, used as a custom hash function for | ||
corresponding abstract types. | ||
|
||
* Functions added | ||
* OCaml: Linexpr0.of_list, Linexpr0.of_array, | ||
Environment.lce_change, Environment.rename_perm | ||
|
||
* Internal functions added/modified | ||
* num: num_integer, numrat_inv added | ||
* apron: spec of ap_texpr0_max_dim modified | ||
|
||
- Distribution/Packaging | ||
* Instruction files REAME.windows and README.mac files, some | ||
problems corrected. | ||
* Makefile.config.model simplified | ||
|
||
- Bugs corrected: several, in particular: | ||
* Special cases with abstract values in dimension 0, and null | ||
arrays in nassign/substitution functions and | ||
add_dimensions/remove_dimensions | ||
* ap_fpu_init for Mac | ||
* itv_lincons_reduce_integer (normalisation of integer constraints) | ||
|
||
Version 0.9.8 | ||
* ap_linexpr0_compare | ||
- New C++ interface, still experimental | ||
|
||
- Instructions for compilation under Windows | ||
|
||
- Clarification of license issues related to the PPL (under GPL license, | ||
whereas APRON is LGPL) | ||
|
||
- Several bugs corrections | ||
|
||
Version 0.9.7 | ||
|
||
Many changes ! | ||
|
||
General: | ||
|
||
- Addition of the reduced product of linear inequalities (from | ||
Polka library) and linear congruences (from PPL library). | ||
|
||
- Addition of tree expressions and constraints, generalizing | ||
linear expressions and constraints with | ||
* non-linear operations (multiplication, division, square root, ...) | ||
* integer, rational/real and floating-point semantics | ||
|
||
C interface: | ||
|
||
- API: | ||
* Addition of ap_abstract1_unify function | ||
* Modification of the signature of ap_environment_remove | ||
|
||
- some (redundant) functions removed from the API requested from | ||
underlying domains, but still provided through the APRON | ||
interface (level 0 and 1) for compatibility reasons: | ||
* of_lincons_array | ||
* assign_linexpr, substitute_linexpr (superseded by | ||
assign_linexpr_array, substitute_linexpr_array). | ||
|
||
- Suffixes of C libraries names indicating internal number | ||
representation made more systematic and uniform among various | ||
underlying libraries: | ||
|
||
* Il, Ill, MPZ: denotes resp. long int, long long int, mpz_t (GMP) | ||
* Rl, Rll, MPQ: denotes resp. rationals using long int, long | ||
long int, and mpq_t (GMP) | ||
* D, Dl: denotes resp. double and long double | ||
|
||
C library name without suffix (eg, libpolka.a) corresponds to | ||
the default suffix MPQ. | ||
|
||
- Other changes in library organisation: | ||
|
||
* libitv.a integrated in libapron.a | ||
* libapron_ppl.a renamed in libap_ppl.a, | ||
libppl_caml.a renamed in libap_ppl_caml.a | ||
|
||
OCaml interface | ||
- Linking simplified thanks to the change in C libraries (see above). | ||
- API: | ||
* Addition of Environment.lce, Abstract1.unify (Abstract1.unify_with) functions | ||
* Modification of the signature of Environment.remove | ||
|
||
Version 0.9.6 | ||
|
||
OCaml interface | ||
- PPL module | ||
- Parsing extended for congruence equalities and congruence generators. | ||
|
||
General: | ||
- Addition of PPL *convex polyhedra* and *linear congruences* | ||
(grids) abstract domains | ||
- Some internal reorganisation | ||
apron/ap_linearize module added | ||
- Full support for interval linear expressions and linearisation to | ||
(quasi-)linear expressions in NewPolka and PPL libraries. Well | ||
tested for quasilinear expressions, not yet for full interval | ||
linear expressions. | ||
- Many bugs corrected. | ||
|
||
Version 0.9.5 | ||
|
||
OCaml interface | ||
- Better type systems, similar to the system used by the [Bigarray] | ||
library of the OCaml standard distribution. | ||
- Generation and installation in $(APRON_PREFIX)/bin of apronrun | ||
and aprontop executables in the main Makefile. | ||
|
||
C interface: | ||
- Use of const qualifier removed in the API, except for strings | ||
(const char *) | ||
|
||
General: | ||
- mpfr library now required in addition to gmp library. | ||
- conversions between mpq_t and double are now safer, thanks to the use of | ||
mpfr. | ||
- itv becomes box. | ||
- package num extended with a new package itv, used currently by box. | ||
- support for linear congruences added in constraints and generators. | ||
- NewPolka offers a layer for linear equalities only, in addition to more | ||
general linear inequalities. | ||
- Improved Makefiles and Makefile.config.model | ||
- Bugs corrected, in particular in Box and Newpolka. | ||
|
||
Version 0.9.4 | ||
|
||
- Modification of Makefile and Makefile.config.model | ||
|
||
- Updated documentation | ||
|
||
- OCaml linking: apron.cmo, polka.cmo, oct.cmo... become libraries | ||
apron.cma, polka.cma,... that reference needed C libraries, with | ||
the exception of libpolkaXX, liboctXX, ... This is documented in | ||
READMEs and doc. | ||
|
||
- mlapronidl: Added string parsing (module Parser) | ||
|
||
- newpolka: | ||
|
||
* Stronger normalization in widening for strict constraints | ||
|
||
* Bug fixed (some of them were severe) | ||
|
Oops, something went wrong.