TP5 - Produit Réduit

The goal of this session is to implement in our analyzer the reduced products between two simple non-relational domains: the interval domain and the parity domain.

Parity domain

A first (straightforward) step is to implement a parity domain, able to discover whether each variable is even or odd. This is the MakeParity functor in int_domain.ml.

Reduction

We wish to implement the reduced product in a generic way, with as few dependencies as possible on the domains we wish to combine.

Constrains

To do that, we defined a common constrain type, in constrain.ml. For all lower-level domains (int_domain bool_domain values), make sur you correctly implemented the following functions

  • get_constrains that returns the set of constrains valid in the abstract value given as argument
  • use_constrains that reduces the abstract value using the set of constrains

To conclude complete the MakeProduct functor in environment.ml. The product of domain have to perform the reduction whenever you feel suited.