Frama-C API - LF_env
Imperative environment to perform fixpoint algorithm for recursive functions. This environnement store four pieces of information associated to every logic_info:
- the current profile in which the interval for the logic_info is infered.
- the current interval that it is infered to.
- a map associating to each parameter all the arguments in their profiles that this parameter has been called with up until now.
- the depth of calls to the fixpoint algorithm associated to the logic_info. When this depth reaches 0, the entry corresponding to the logic_info is cleared thus avoiding unification between two independent calls to the same logic function, which is unsafe.
The third argument is used so that whenever a parameter of a logic_info is unified by widening with a new value, the interval inference algorithm updates all the arguments that this parameter have been called with, to assign the new interval to it
val find_profile : Frama_c_kernel.Cil_types.logic_info -> Profile.t
find the current profile in which a recursive function or predicate is being infered
val find_ival : Frama_c_kernel.Cil_types.logic_info -> Analyses_types.ival
find the currently inferred interval for a call to a logic function
val find_profile_ival : Frama_c_kernel.Cil_types.logic_info -> Profile.t * Analyses_types.ival
return the pair of both the results of find_profile
and find_ival
val find_args : Frama_c_kernel.Cil_types.logic_info -> Profile.t Misc.Id_term.Map.t Frama_c_kernel.Cil_datatype.Logic_var.Map.t
find all the arguments a recursive function or predicate has been called with
val add : logic_env:Logic_env.t -> Frama_c_kernel.Cil_types.logic_info -> Profile.t -> Analyses_types.ival -> Frama_c_kernel.Cil_types.term list -> unit
add ival
as the current one for a logic function or predicate call
val decrease : Frama_c_kernel.Cil_types.logic_info -> unit
decrease the counter of fixpoint depth
val update_ival : Frama_c_kernel.Cil_types.logic_info -> Analyses_types.ival -> unit
update the current interval for the a given logic_info
val is_rec : Frama_c_kernel.Cil_types.logic_info -> bool
determine whether a logic function or predicate is recursive