Frama-C API - Logic_env
logic environment: interval of all bound variables. It consists in two components
- a profile for variables bound through function arguments
- an association list for variables bound by a let or a quantification
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