Box (box.h): intervals abstract domain

The BOX interval library is aimed to be used through the APRON interface.

Use of Box

To use BOX in C, add

#include "box.h"

in your source file(s) and add ‘-I$(BOX_PREFIX)/include’ in the command line in your Makefile.

You should also link your object files with the BOX library to produce an executable, by adding something like ‘-L$(APRON_PREFIX)/lib -lboxmpq -litvmpq’ in the command line in your Makefile (followed by the standard ‘-lapron -litvmpq -litvdbl -L$(MPFR_PREFIX)/lib -lmpfr -L$(GMP_PREFIX)/lib -lgmp’).

There are actually several variants of the library:

libboxllr.a

The underlying representation for numbers is rationals based on long long int integers. This may cause overflows. These are currently not detected. It requires also the libitvllr.a library.

libboxdbl.a

The underlying representations for numbers is double. Overflows are not possible (we use infinite floating numbers), but currently the soundness is not ensured for all operations. It requires also the libitvdbl.a library.

libboxmpq.a

The underlying representations for rationams is mpq_t, the multi-precision rationals from the GNU GMP library. Overflows are not possible any more, but huge numbers may appear. It requires also the libitvmpq.a library.

Also, all library are available in debug mode (‘libboxmpq_debug.a’, ...).

Allocating Box managers

Function: ap_manager_t* box_manager_alloc ()

Allocate a APRON manager linked to the Box library.