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.