forked from antoinemine/apron
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Changes
319 lines (217 loc) · 9.56 KB
/
Changes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
Version 0.9.14
- Add support for PPLite 0.11 polyhedra library [Enea Zaffanella] (#71)
- Add Fppol domain (floating-point polyhedra) [Liqian Chen] (#33)
- Add Avoct domain (absolute value octagons) [Liqian Chen] (#33)
- Add OCaml 5.0.0 support
- Replace quicksort implementation with a new, LGPL one (#87)
- make install installs non-debug version only, unless -debug is used (#86)
- Non-debug C libraries are stripped (#86)
- Compilation and installation fixes (#80, #75, #65, #62, #61, #60, #59, #54, #52, #49, #48, #45, #34)
- Apple M1 support (#68)
- Fix some corner cases for boxes and polyhedra (#85, #83, #82, #81, #80, #63, #43, #35)
- Fix level 1 fold (#90)
Version 0.9.13
- Fix Java version detection & compilation (#30)
- Minor grammar and spelling fixes (#22), (#26)
- Use texi2any instead of (dead) texi2html (#23)
- Fix best and exact flags in octagons (#25)
- Fix linking under MaxOS X (#28)
- Taylor1+ fixes
Version 0.9.12
- GitHub hosting
- Documentation hosted on GitHub Pages
- New installation instructions for Windows
- Opam package (ocaml)
- Added a function to get the version number
- Several bugs corrected
Version 0.9.11
- New domain: Taylor1plus (aka zonotopes), provided by CEA LIST
Version 0.9.10
- Migration advices (due to some API and compilation process changes)
* as MLGMPIDL is not included anymore, you may want to consider
- either apron-dist-XXX.tgz packages
- or svn co http://svn.cri.ensmp.fr/svn/apron/apron-dist/trunk apron-dist
that include it.
* Makefile.config:
° new variables HAS_SHARED and OCAMLMKLIB
* 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
- Distribution/Packaging
* MLGMPIDL not included anymore.
If you want to include it with apron, consider:
- either apron-dist-XXX.tgz packages
- or svn co http://svn.cri.ensmp.fr/svn/apron/apron-dist/trunk apron-dist
* 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.
- 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
- 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)