module Separation:sig
..end
type
region =
| |
Var of |
(* |
the variable,
&x | *) |
| |
Ptr of |
(* |
the cell pointed by
p | *) |
| |
Arr of |
(* |
the array around
p | *) |
val pp_region : Format.formatter -> region -> unit
type
clause = {
|
mutex : |
|
other : |
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
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
is_true
clausesval pp_clause : Format.formatter -> clause -> unit