Merge branch 'master' into fix/java-new-finalizer

COPYING

@@ -29,6 +29,10 @@ of the original package are not covered by the License described in this
 file. They are distributed under the GNU General Public License version 2,
 included in the COPYING file contained in those subdirectories.
 
+The files contained in the pplite subdirectory of the original package
+are not covered by the License described in this file. They are distributed
+under the GNU General Public License version 3, included in the COPYING
+file contained in those subdirectories.
 
 ----------------------------------------------------------------------
 

Changes

@@ -1,9 +1,52 @@
+Version 0.9.15
+
+- BREAKING CHANGE FOR OCAML: remove polymorphic compare functions and renamed compare functions that do not implement a total order, documentation clarification (#108)
+
+- Autodetect library in configure for Mac ARM with Homebrew (#107)
+
+- Support for PPLite 0.12 [Michele Spotti, Enea Zaffanella] (#105)
+
+- Disable PPL and PPLite when no C++ compiler is detected (#104)
+
+- Various fixes (#101, #97, #90)
+
+
+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
 
 

Makefile

@@ -26,6 +26,9 @@ c:
 ifneq ($(HAS_PPL),)
 	(cd ppl; $(MAKE))
 	(cd products; $(MAKE))
+endif
+ifneq ($(HAS_PPLITE),)
+	(cd pplite; $(MAKE))
 endif
 	(cd avoct; $(MAKE) MPQ D)
 ifneq ($(HAS_GLPK),)
@@ -47,6 +50,9 @@ ml:
 ifneq ($(HAS_PPL),)
 	(cd ppl; $(MAKE) ml)
 	(cd products; $(MAKE) ml)
+endif
+ifneq ($(HAS_PPLITE),)
+	(cd pplite; $(MAKE) ml)
 endif
 	(cd avoct; $(MAKE) mlMPQ mlD)
 ifneq ($(HAS_GLPK),)
@@ -61,15 +67,21 @@ apronppltop:
 	$(OCAMLMKTOP) -I $(MLGMPIDL_LIB) -I $(APRON_LIB) -verbose -o $@ \
 	bigarray.cma gmp.cma apron.cma boxMPQ.cma octMPQ.cma polkaMPQ.cma ppl.cma polkaGrid.cma t1pMPQ.cmxa avoMPQ.cma
 
+apronpplitetop:
+	$(OCAMLMKTOP) -I $(MLGMPIDL_LIB) -I $(APRON_LIB) -verbose -o $@ \
+	bigarray.cma gmp.cma apron.cma boxMPQ.cma octMPQ.cma polkaMPQ.cma pplite.cma t1pMPQ.cmxa avoMPQ.cma
+
 apronglpktop:
 	$(OCAMLMKTOP) -I $(MLGMPIDL_LIB) -I $(APRON_LIB) -verbose -o $@ \
 	bigarray.cma gmp.cma apron.cma boxMPQ.cma octMPQ.cma polkaMPQ.cma t1pMPQ.cma avoMPQ.cma fppMPQ.cma
 
 rebuild:
 	@echo "$(MAKE) rebuild is no longer necessary"
 
-OCAMLFIND_PROTO = xxx.cma $(call OCAMLOPT_TARGETS, xxx) libxxx_caml.a	\
-		  libxxx_caml_debug.a
+OCAMLFIND_PROTO = xxx.cma $(call OCAMLOPT_TARGETS, xxx) libxxx_caml.a
+ifneq ($(HAS_DEBUG),)
+OCAMLFIND_PROTO += $(call OCAMLOPT_TARGETS, xxx.d)  libxxx_caml_debug.a
+endif
 ifneq ($(HAS_SHARED),)
 OCAMLFIND_PROTO += dllxxx_caml.$(EXT_DLL)
 endif
@@ -101,10 +113,14 @@ disjunction) \
 
 ifneq ($(HAS_PPL),)
 OCAMLFIND_FILES += \
-	$(patsubst %,ppl/%, ppl.idl ppl.mli ppl.cmi ppl.cma ppl.cmx $(call OCAMLOPT_TARGETS, ppl) libap_ppl_caml.a libap_ppl_caml_debug.a dllap_ppl_caml.$(EXT_DLL)) \
+	$(patsubst %,ppl/%, ppl.idl ppl.mli ppl.cmi ppl.cma ppl.cmx $(call OCAMLOPT_TARGETS, ppl) libap_ppl_caml.a dllap_ppl_caml.$(EXT_DLL)) \
 	$(patsubst %,products/%, polkaGrid.idl polkaGrid.mli polkaGrid.cmi polkaGrid.cmx) \
 	$(patsubst %,products/%, $(subst xxx,polkaGrid, $(OCAMLFIND_PROTO)))
 endif
+ifneq ($(HAS_PPLITE),)
+OCAMLFIND_FILES += \
+	$(patsubst %,pplite/%, pplite.idl pplite.mli pplite.cmi pplite.cma pplite.cmx $(call OCAMLOPT_TARGETS, pplite) libap_pplite_caml.a dllap_pplite_caml.$(EXT_DLL))
+endif
 ifneq ($(HAS_GLPK),)
 OCAMLFIND_FILES += \
 	$(patsubst %,fppol/%, fpp.mli fpp.cmi fpp.cmx) \
@@ -123,6 +139,10 @@ ifneq ($(HAS_PPL),)
 OCAMLFIND_FILES += \
 	$(patsubst %,ppl/%, ppl.cmti ppl.cmt) \
 	$(patsubst %,products/%, polkaGrid.cmti polkaGrid.cmt)
+endif
+ifneq ($(HAS_PPLITE),)
+OCAMLFIND_FILES += \
+	$(patsubst %,pplite/%, pplite.cmti pplite.cmt)
 endif
 	$(patsubst %,avoct/%, avo.cmti avo.cmt)
 ifneq ($(HAS_GLPK),)
@@ -142,6 +162,9 @@ install: all
 ifneq ($(HAS_PPL),)
 	(cd ppl; $(MAKE) install)
 	(cd products; $(MAKE) install)
+endif
+ifneq ($(HAS_PPLITE),)
+	(cd pplite; $(MAKE) install)
 endif
 	(cd avoct; $(MAKE) install)
 ifneq ($(HAS_GLPK),)
@@ -155,16 +178,15 @@ ifeq ($(OCAMLFIND),)
 ifneq ($(HAS_PPL),)
 	if test -f apronppltop; then $(INSTALL) apronppltop $(APRON_BIN); fi
 endif
+ifneq ($(HAS_PPLITE),)
+	if test -f apronpplitetop; then $(INSTALL) apronpplitetop $(APRON_BIN); fi
+endif
 ifneq ($(HAS_GLPK),)
 		if test -f apronglpktop; then $(INSTALL) apronglpktop $(APRON_BIN); fi
 endif
 else
 	$(OCAMLFIND) remove apron
-	$(OCAMLFIND) install apron mlapronidl/META $(OCAMLFIND_FILES)	\
-		$(call OCAMLOPT_TARGETS, mlapronidl/apron.d		\
-					 newpolka/polkaMPQ.d		\
-					 newpolka/polkaRll.d		\
-					 taylor1plus/t1pMPQ.d taylor1plus/t1pD.d taylor1plus/t1pMPFR.d)
+	$(OCAMLFIND) install apron mlapronidl/META $(OCAMLFIND_FILES)
 endif
 endif
 ifneq ($(HAS_CPP),)
@@ -175,11 +197,14 @@ ifneq ($(HAS_JAVA),)
 endif
 
 ifneq ($(OCAMLFIND),)
-install: mlapronidl/META
-mlapronidl/META: mlapronidl/META.in mlapronidl/META.ppl.in
+ml: mlapronidl/META
+mlapronidl/META: mlapronidl/META.in mlapronidl/META.ppl.in mlapronidl/META.pplite.in
 	$(SED) -e "s!@VERSION@!$(VERSION_STR)!g;" $< > $@;
   ifneq ($(HAS_PPL),)
 	cat mlapronidl/META.ppl.in >> $@;
+  endif
+  ifneq ($(HAS_PPLITE),)
+	cat mlapronidl/META.pplite.in >> $@;
   endif
 	$(SED) -e '/^[[:space:]]*archive(byte)/ { p; s ) ,plugin) ;}' -i.bak $@;
   ifneq ($(HAS_NATIVE_PLUGINS),)
@@ -199,14 +224,15 @@ clean:
 	(cd octagons; $(MAKE) clean)
 	(cd taylor1plus; $(MAKE) clean)
 	(cd ppl; $(MAKE) clean)
+	(cd pplite; $(MAKE) clean)
 	(cd products; $(MAKE) clean)
 	(cd avoct; $(MAKE) clean)
 	(cd fppol; $(MAKE) clean) 
 	(cd apronxx; $(MAKE) clean)
 	(cd examples; $(MAKE) clean)
 	(cd test; $(MAKE) clean)
 	(cd japron; $(MAKE) clean)
-	rm -fr online tmp apron*run aprontop apronppltop apronglpktop
+	rm -fr online tmp apron*run aprontop apronppltop apronpplitetop apronglpktop
 	rm -f mlapronidl/META
 
 distclean: clean
@@ -223,6 +249,7 @@ uninstall:
 	(cd taylor1plus; $(MAKE) uninstall)
 	(cd examples; $(MAKE) uninstall)
 	(cd ppl; $(MAKE) uninstall)
+	(cd pplite; $(MAKE) uninstall)
 	(cd products; $(MAKE) uninstall)
 	(cd avoct; $(MAKE) uninstall)
 	(cd fppol; $(MAKE) uninstall) 
@@ -249,7 +276,7 @@ endif
 
 PKG  = $(PKGNAME)-$(VERSION_STR)
 PKGFILES = Makefile README README.windows README.mac AUTHORS COPYING Makefile.config.model Changes configure vars.mk ocamlpack
-PKGDIRS  = apron num itv octagons box newpolka taylor1plus ppl products avoct fppol mlapronidl examples test apronxx japron
+PKGDIRS  = apron num itv octagons box newpolka taylor1plus ppl pplite products avoct fppol mlapronidl examples test apronxx japron
 
 dist:
 	$(MAKE) all

Makefile.config.model

@@ -21,6 +21,10 @@ HAS_OCAMLOPT = 1
 
 # HAS_PPL = 1
 
+# If defined to non-empty value, enable domains from the PPLite library
+
+# HAS_PPLITE = 1
+
 # If defined to non-empty value, compiles the fppol domain
 # (The fppol domain requires GLPK)
 
@@ -68,6 +72,14 @@ MPFR_PREFIX = /usr
 #
 PPL_PREFIX = /usr
 
+# Where to find FLINT ($(FLINT_PREFIX)/include, ($FLINT_PREFIX)/lib
+# (only required by PPLite)
+FLINT_PREFIX = /usr
+
+# Where to find PPLITE ($(PPLITE_PREFIX)/include, $(PPLITE_PREFIX)/lib
+#
+PPLITE_PREFIX = /usr
+
 # Where to find GLPK ($(GLPK_PREFIX)/include, $(GLPK_PREFIX)/lib
 #
 GLPK_PREFIX = /usr
@@ -159,11 +171,18 @@ CXXFLAGS_DEBUG = \
 -Wno-unused -Wno-unused-parameter -Wno-unused-function \
 -fPIC -g -O0 -UNDEBUG
 
+# The PPLite wrapper requires using the C++11 language standard
+# (note: building PPLite from sources requires the C++17 language standard)
+PPLITE_CXXFLAGS = -std=c++11 $CXXFLAGS
+PPLITE_CXXFLAGS_DEBUG = -std=c++11 $CXXFLAGS_DEBUG
+
+
 AR = ar
 RANLIB = ranlib
 SED = sed
 PERL = perl
 INSTALL = install
+INSTALLSTRIP = install --strip
 INSTALLd = install -d
 
 OCAMLC = ocamlc.opt

README.md

@@ -21,10 +21,10 @@ Apron includes the following numeric domains:
 * octagons
 * zonotopes (taylor1plus)
 
-Additional domains are made available through the optional PPL third-party library:
-* alternate polyhedra implementation
-* grids
-* reduced products of polyhedra and grids
+Additional domains are made available through the optional PPL and PPLite third-party libraries:
+* alternate polyhedra implementation (PPL, PPLite)
+* grids (PPL)
+* reduced products of polyhedra and grids (PPL)
 
 The domains are made available under a common interface, so that changing the abstract domain of interpretation in a static analysis should only take a one-line change.
 
@@ -50,6 +50,14 @@ Compiling the built-in domains with the C interface requires:
 
 Compiling the PPL-based domains requires the [Parma Polyhedra Library](http://bugseng.com/products/ppl) (tested with version 1.2) and gcc (no clang).
 
+Compiling the PPLite-based domains requires the
+[PPLite library](https://github.com/ezaffanella/PPLite),
+which also depends on Flint.
+Note that building the PPLite library from sources requires using a
+C++ compiler (g++ or clang++) that supports the c++17 language standard;
+however, starting from PPLite version 0.11, the Apron wrapper for PPLite
+can be compiled using a C++ compiler supporting the c++11 language standard.
+
 
 ### Additional language support
 
@@ -91,10 +99,22 @@ In case some components fail to compile, it is possible to disable them through
 * `-no-java` to disable the Java API (there are known problems where the compilation fails to find `jni.h` )
 * `-no-ocaml` to disable the OCaml API
 * `-no-ppl` to disable the PPL domains
+* `-no-pplite` to disable the PPLite domains
 
 See `./configure -help` for more options.
 
 
+### Debug versions
+
+By default, `make install` now only install non-debug versions of the C libraries.
+Moreover, these are striped of symbols.
+
+Use the `-debug` `./configure` option to also install debug (non-stripped) C versions, and `-no-strip` to avoid stripping the non-debug C versions.
+The C debug versions have a `_debug` suffix (such as `libapron_debug.so`).
+
+When installing with `opam`, debug versions are always available.
+OCaml debug libraries use the `.d` suffix (such as `apron.d.cmxa`).
+
 
 ### Installation on MacOS X
 

apron.opam

@@ -5,7 +5,7 @@ authors: [
   "Antoine Miné"
   "https://github.com/antoinemine/apron/graphs/contributors"
 ]
-license: "LGPL-2.1 with linking exception"
+license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception"
 homepage: "https://antoinemine.github.io/Apron/doc/"
 maintainer: "Nicolas Berthier <[email protected]>"
 dev-repo: "git+https://github.com/antoinemine/apron.git"
@@ -20,6 +20,8 @@ build: [
     "--no-ocaml-plugins" {os = "freebsd"}
     "--absolute-dylibs" {os = "macos"}
     "--ext-dll" {os = "win32"} "dll" {os = "win32"}
+    "--debug"
+    "--no-strip"
   ]
   [make "-j%{jobs}%"]
 ]

apron/Makefile

@@ -53,12 +53,14 @@ LDFLAGS += $(MP_LIFLAGS) -lm -lmpfr -lgmp
 # Rules
 #---------------------------------------
 
-LIB_FILES = libapron.a libapron_debug.a
+LIB_FILES = libapron.a
+LIB_FILES_DEBUG = libapron_debug.a
 ifneq ($(HAS_SHARED),)
-LIB_FILES += libapron.$(EXT_DLL) libapron_debug.$(EXT_DLL)
+LIB_FILES += libapron.$(EXT_DLL)
+LIB_FILES_DEBUG += libapron_debug.$(EXT_DLL)
 endif
 
-all: $(LIB_FILES)
+all: $(LIB_FILES) $(LIB_FILES_DEBUG)
 
 #---------------------------------------
 # Misc rules
@@ -71,7 +73,7 @@ dist: $(H_FILES) $(C_FILES) $(CH_FILES_AUX) apron.texi Makefile COPYING README a
 	(cd ..; tar zcvf apron.tgz $(^:%=apron/%))
 
 clean:
-	/bin/rm -f *.aux *.bbl *.blg *.dvi *.log *.toc *.ps *.pdf apron.cps apron.fns apron.info apron.fn apron.ky apron.pg apron.cp apron.tp apron.vr apron.kys apron.pgs apron.tps apron.vrs newpolka.texi box.texi ap_ppl.texi ap_pkgrid.texi apron.info* depend ap_version.h
+	/bin/rm -f *.aux *.bbl *.blg *.dvi *.log *.toc *.ps *.pdf apron.cps apron.fns apron.info apron.fn apron.ky apron.pg apron.cp apron.tp apron.vr apron.kys apron.pgs apron.tps apron.vrs newpolka.texi box.texi ap_ppl.texi ap_pplite.texi ap_pkgrid.texi apron.info* depend ap_version.h
 	/bin/rm -f *.o *.a *.cmi *.cmo *.cmx *.cmx[as] *.cma *.$(EXT_DLL)
 	/bin/rm -fr html
 	/bin/rm -f apron.pdf rationale.pdf
@@ -82,7 +84,10 @@ install: all
 	mkdir -p $(APRON_INCLUDE)
 	cp $(H_FILES) $(APRON_INCLUDE)
 	mkdir -p $(APRON_LIB)
-	for i in $(LIB_FILES); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done
+	for i in $(LIB_FILES); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); $(STRIP) $(APRON_LIB)/$$i;  fi; done
+ifneq ($(HAS_DEBUG),)
+	for i in $(LIB_FILES_DEBUG); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done
+endif
 
 uninstall:
 	/bin/rm -f $(H_FILES:%=$(APRON_INCLUDE)/%)
@@ -101,19 +106,21 @@ ap_pkgrid.texi: ../products/ap_pkgrid.texi
 	ln -sf $< $@
 ap_ppl.texi: ../ppl/ap_ppl.texi
 	ln -sf $< $@
+ap_pplite.texi: ../pplite/ap_pplite.texi
+	ln -sf $< $@
 newpolka.texi: ../newpolka/newpolka.texi
 	ln -sf $< $@
 box.texi: ../box/box.texi
 	ln -sf $< $@
 
-apron.pdf: apron.texi rationale.texi ../products/ap_pkgrid.texi ../ppl/ap_ppl.texi ../newpolka/newpolka.texi ../box/box.texi 
+apron.pdf: apron.texi rationale.texi ../products/ap_pkgrid.texi ../ppl/ap_ppl.texi ../pplite/ap_pplite.texi ../newpolka/newpolka.texi ../box/box.texi 
 	$(TEXI2ANY) --pdf -o $@ $<
 
-apron.info: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi newpolka.texi box.texi
+apron.info: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi ap_pplite.texi newpolka.texi box.texi
 	$(MAKEINFO) -o $@ $<
 
 
-html: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi newpolka.texi box.texi 
+html: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi ap_pplite.texi newpolka.texi box.texi 
 	$(TEXI2ANY) -o html --html --split=section --no-number-sections $<
 	cp -f ../octagons/oct_doc.html html
 	cp -f ../examples/*.c ../examples/*.ml html