Module Separation

module Separation: sig .. end

type param = 
| NotUsed
| ByAddr
| ByValue
| ByShift
| ByRef
| InContext
| InArray
val pp_param : Format.formatter -> param -> unit
type partition 
type clause 
val empty : partition
val set : Cil_types.varinfo ->
param -> partition -> partition
val requires : partition -> clause

Build the separation clause from a partition

val is_true : clause -> bool
val filter : clause list -> clause list

Only non-trivial clauses

val pp_clause : Format.formatter -> clause -> unit

Prints the separation in ACSL format.