Make (frama-c-inout.Inout.Cumulative

Parameters

module X : sig ... end

Signature

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