Analyses_datatype.LF_env
Imperative environment to perform the fixpoint algorithm for recursive functions
val find :
Frama_c_kernel.Cil_types.logic_info ->
Profile.t ->
Analyses_types.ival
find the currently inferred interval for a call to a logic function
clear the table of intervals for logic function (to do between typing ) each logic function calls
val add :
Frama_c_kernel.Cil_types.logic_info ->
Profile.t ->
Analyses_types.ival ->
unit
add an interval as the current one for a logic function call
val add_pred : Frama_c_kernel.Cil_types.logic_info -> Profile.t -> unit
add 0..1 as the current interval for a predicate call
val is_rec : Frama_c_kernel.Cil_types.logic_info -> bool
determine whether a logic function or predicate is recursive
val replace :
Frama_c_kernel.Cil_types.logic_info ->
Profile.t ->
Analyses_types.ival ->
unit
replace the current interval for a logic function call