Previous  Up  Next

Module Separation

module Separation: sig .. end
Elementary regions
type region =
| Var of Cil_types.varinfo (*
the variable, &x
*)
| Ptr of Cil_types.varinfo (*
the cell pointed by p
*)
| Arr of Cil_types.varinfo (*
the array around p
*)
Elementary regions
val pp_region : Format.formatter -> region -> unit
Prints region in ACSL format
type clause = {
   mutex : region list;
   other : region list;
}
List of regions to be separated. The ACSL interpretation of this compact separation clause is: 
    //@ requires: \separated(mutex_1, ..., mutex_n, \union(other_1, ..., other_m) );
Such a specification actually consists of (n-1)*n/2 + n*m elementary separation clauses.
val is_true : clause -> bool
Returns true if the clause is degenerated. This occurs when mutex is empty, or when mutex is a singleton and other is empty.
val requires : clause list -> clause list
Filter out is_true clauses
val pp_clause : Format.formatter -> clause -> unit
Prints the separation in ACSL format.