Module 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

find the current profile in which a recursive function or predicate is being infered

find the currently inferred interval for a call to a logic function

return the pair of both the results of find_profile and find_ival

find all the arguments a recursive function or predicate has been called with

val clear : unit -> unit

clear the table of intervals for logic function

add ival as the current one for a logic function or predicate call

decrease the counter of fixpoint depth

update the current interval for the a given logic_info

determine whether a logic function or predicate is recursive