Module Analyses_datatype.Logic_env

logic environment: interval of all bound variables. It consists in two components

type t
val ival_meet_ref : (Analyses_types.ival -> Analyses_types.ival -> Analyses_types.ival) Stdlib.ref

forward reference to meet of intervals

add a new binding for a let or a quantification binder only

val empty : t

the empty environment

val make : Profile.t -> t

create a new environment from a profile, for function calls

find a logic variable in the environment

val get_profile : t -> Profile.t

get the profile of the logic environment, i.e. bindings through function arguments

refine the interval of a logic variable: replace an interval with a more precise one