Frama-C API - Bvars
Bound Variables Footprints.
All provided operation are constant-time bitwise and integer operations.
val empty : t
val singleton : int -> t
val order : t -> int
Max stack of binders
val closed : t -> bool
All variables are bound
val closed_at : int -> t -> bool
closed_at n a
Does not contains variables k<n
val is_empty : t -> bool
No bound variables
val contains : int -> t -> bool
if contains k s
returns false
then k
does not belong to s
val overlap : int -> int -> t -> bool
if may_overlap k n s
returns false
then no variable i
with k<=i<k+n
occurs in s
.
val pretty : Stdlib.Format.formatter -> t -> unit