Skip to content

Commit

Permalink
New README and installation instructions.
Browse files Browse the repository at this point in the history
  • Loading branch information
antoinemine committed Jan 10, 2019
1 parent 4c4b065 commit 908cf22
Show file tree
Hide file tree
Showing 6 changed files with 225 additions and 86 deletions.
105 changes: 105 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,105 @@
*.o
*.a
*.exe
*.so
*.class
*.jar

Makefile.config
*.cm?
*.cmx?
*~
*#
**/depend
**/tmp
apronxx/apronxx_test
box/box.ml
box/box.mli
box/box_caml.c
japron/apron/apron_*.h
japron/gmp/gmp_*.h
mlapronidl/abstract0.ml
mlapronidl/abstract0.mli
mlapronidl/abstract0_caml.c
mlapronidl/abstract1.ml
mlapronidl/abstract1.mli
mlapronidl/abstract1_caml.c
mlapronidl/apron_lexer.ml
mlapronidl/apron_ocamldoc.mli
mlapronidl/apron_parser.ml
mlapronidl/apron_parser.mli
mlapronidl/coeff.ml
mlapronidl/coeff.mli
mlapronidl/coeff_caml.c
mlapronidl/dim.ml
mlapronidl/dim.mli
mlapronidl/dim_caml.c
mlapronidl/disjunction.ml
mlapronidl/disjunction.mli
mlapronidl/disjunction_caml.c
mlapronidl/environment.ml
mlapronidl/environment.mli
mlapronidl/environment_caml.c
mlapronidl/generator0.ml
mlapronidl/generator0.mli
mlapronidl/generator0_caml.c
mlapronidl/generator1.ml
mlapronidl/generator1.mli
mlapronidl/generator1_caml.c
mlapronidl/interval.ml
mlapronidl/interval.mli
mlapronidl/interval_caml.c
mlapronidl/lincons0.ml
mlapronidl/lincons0.mli
mlapronidl/lincons0_caml.c
mlapronidl/lincons1.ml
mlapronidl/lincons1.mli
mlapronidl/lincons1_caml.c
mlapronidl/linexpr0.ml
mlapronidl/linexpr0.mli
mlapronidl/linexpr0_caml.c
mlapronidl/linexpr1.ml
mlapronidl/linexpr1.mli
mlapronidl/linexpr1_caml.c
mlapronidl/manager.ml
mlapronidl/manager.mli
mlapronidl/manager_caml.c
mlapronidl/policy.ml
mlapronidl/policy.mli
mlapronidl/policy_caml.c
mlapronidl/scalar.ml
mlapronidl/scalar.mli
mlapronidl/scalar_caml.c
mlapronidl/tcons0.ml
mlapronidl/tcons0.mli
mlapronidl/tcons0_caml.c
mlapronidl/tcons1.ml
mlapronidl/tcons1.mli
mlapronidl/tcons1_caml.c
mlapronidl/texpr0.ml
mlapronidl/texpr0.mli
mlapronidl/texpr0_caml.c
mlapronidl/texpr1.ml
mlapronidl/texpr1.mli
mlapronidl/texpr1_caml.c
mlapronidl/var.ml
mlapronidl/var.mli
mlapronidl/var_caml.c
newpolka/polka.ml
newpolka/polka.mli
newpolka/polka_caml.c
octagons/oct.ml
octagons/oct.mli
octagons/oct_caml.c
octagons/oct*
ppl/ap_ppl_caml.c
ppl/ap_ppl_test
ppl/ppl.ml
ppl/ppl.mli
products/polkaGrid.ml
products/polkaGrid.mli
products/polkaGrid_caml.c
taylor1plus/t1p.ml
taylor1plus/t1p.mli
taylor1plus/t1p_caml.c

8 changes: 8 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -240,3 +240,11 @@ pkg_%:
rm -rf $*.tgz

.NOTPARALLEL:

Makefile.config:
@echo
@echo "***"
@echo "*** Run ./configure first to generate a Makefile.config"
@echo "***"
@echo
@exit 1
86 changes: 0 additions & 86 deletions README

This file was deleted.

3 changes: 3 additions & 0 deletions README.mac
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
This document is no longer up to date.

---------------

This document tries to explain some specific points in compiling Apron under
Macintosh. It brings additional information compared to the README.
Expand Down
106 changes: 106 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
# The Apron Numerical Abstract Domain Library

## Introduction

Apron is a library to represent properties of numeric variables, such as variable bounds or linear relations between variables, and to manipulate these properties through semantic operations, such as variable assignments, tests, conjunctions, entailment.

Apron is intended to be used in static program analyzers, in order to infer invariants of numeric variables, i.e., properties that hold for all executions of a program. It is based on the theory of Abstract Interpretation.


## Overview

The Apron library includes several numeric abstract domains, corresponding to different classes of numeric properties with their own internal representation and algorithms, achieving various trade-offs between precision, expressiveness, and efficiency.

Apron includes the following numeric domains:
* intervals (boxes)
* polyhedra (newpolka)
* 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

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.

The core API is in C, but optional API wrappers for additional languages are provided:
* OCaml
* Java
* C++


## Dependencies

### Base

Compiling the built-in domains with the C interface requires:
* a C compiler (gcc or clang)
* [https://gmplib.org/](GMP) version 5 or later, with development files
* [https://www.mpfr.org/](MPFR) version 3 or later, with development files
* perl
* sed


### Additional domains

Compiling the PPL-based domains requires the [Parma Polyhedra Library](http://bugseng.com/products/ppl) (tested with version 1.2) and gcc (no clang).


### Additional language support

Additional language wrappers require additional components:
* a C++ compiler for the C++ API
* a JDK >= 1.6 for the Java API
* for the OCaml API:
* a recent OCaml compiler (tested with 4.07, but earlier 4.x should also work)
* ocamlfind
* camlidl
* mlgmpidl


### Documentation

**Help needed to explain how to generate Apron's API documentation.**


## Installation instructions


### Installation on Linux

On deb-based Linux distributions (Debian, Ubuntu) a `sudo apt-get install libgmp-dev libmpfr-dev` should suffice to get the dependencies for the basic C library.

On Opam-based OCaml distributions, a `opam install ocamlfind camlidl mlgmpidl` should suffice to get the dependencies for the OCaml API.

Compilation from source could be as simple as:
* `./configure`
* `make`
* `sudo make install`

`./configure` automatically generates a `Makefile.config` file. It is also possible to write a `Makefile.config` by hand by taking some inspiration from `Makefile.config.model`.

In case some components fail to compile, it is possible to disable them through `./configure` options:
* `-no-cxx` to disable the C++ API
* `-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

See `./configure -help` for more options.



### Installation on MacOS X

**Help needed for this section.**

The README.mac file is not up to date.



### Installation on Windows

**Help needed for this section.**

The README.windows file is not up to date.

3 changes: 3 additions & 0 deletions README.windows
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
This document is no longer up to date.

---------------

This document tries to explain how to compile Apron under Windows.
For the moment, only 32-bit compilation using the Cygwin environment is
Expand Down

0 comments on commit 908cf22

Please sign in to comment.