Analyses_datatype.LF_env
Imperative environment to perform fixpoint algorithm for recursive functions. This environnement store four pieces of information associated to every logic_info:
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.Hashtbl.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