Cumulative_analysis.Make
module X : sig ... end
module Memo : sig ... end
Module that contains the memoized results
class do_it_cached : Frama_c_kernel.Kernel_function.t list -> object ... end
Class that implements a cached version of the above analysis. Recursion in the dynamic call graphs are handled, provided the value analysis terminated without detecting a real recursion
val kernel_function : Frama_c_kernel.Cil_types.kernel_function -> X.t
Effects of the given kernel_function, using memoization
val statement : Frama_c_kernel.Cil_types.stmt -> X.t
Effects of a statement, using memoization if it contains a function call
val expr : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.exp -> X.t
Effects of the given expression (which is supposed to be at the given statement