Logic_env (frama-c-e-acsl.E_ACSL.Analyses_datatype.Logic

type t

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 make : Profile.t -> t

create a new environment from a profile, for function calls

val find : t -> Frama_c_kernel.Cil_types.logic_var -> Analyses_types.ival

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

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