TP4 - Analyse Relationelle

The goal of this session is to analyze the language developed in the previous sessions using relational numerical abstract domains, in particular the polyhedra domain. However, the Apron library is not documented and terrible to use. So you will write from scratch your own equality abstract domain.

In the previous session, we developed an interval analyzer. In this session we will:

  • Build an abstract domain for equality in module MakeEquality. Since it is a relational domain, it is an implementation of Environment signature.

  • Test your analyzer and evaluate experimentally on simple examples the precision improvements brought by a relational analysis.

  • Adds support for disequalities in MakeEquality.

As the Apron library provides a generic interface, it should be easy for your analyzer to support all the other abstract domains offered by Apron (such as octagons for instance) and perform additional experiments.

Documentation: