Analyses_datatype.Logic_env
logic environment: interval of all bound variables. It consists in two components
val ival_meet_ref :
(Analyses_types.ival ->
Analyses_types.ival ->
Analyses_types.ival)
Stdlib.ref
forward reference to meet of intervals
val add : t -> Frama_c_kernel.Cil_types.logic_var -> Analyses_types.ival -> t
add a new binding for a let or a quantification binder only
val empty : t
the empty environment
val find : t -> Frama_c_kernel.Cil_types.logic_var -> Analyses_types.ival
find a logic variable in the environment
get the profile of the logic environment, i.e. bindings through function arguments
val refine :
t ->
Frama_c_kernel.Cil_types.logic_var ->
Analyses_types.ival ->
t
refine the interval of a logic variable: replace an interval with a more precise one