Module Cumulative_analysis

module Cumulative_analysis: sig .. end

Implementation of a simple meta-analysis on top of the results of the value analysis. This implementation correctly handles memoization and apparent recursive calls during the value analysis.

The underlying analysis is supposed to be cumulative at the level of a kernel_function (its results are derived from the results on all its statements), and mostly non-contextual (all the informations can be gathered using a Cil visitor).

Implementation of a simple meta-analysis on top of the results of the value analysis. This implementation correctly handles memoization and apparent recursive calls during the value analysis.

val specialize_state_on_call : ?stmt:Cil_types.stmt -> Cil_types.kernel_function -> Db.Value.state

If the given statement is a call to the given function, enrich the superposed memory state at this statement with the formal arguments of this function. This is usually more precise than the superposition of all initial states of the function

class virtual ['a] cumulative_visitor : object .. end

Frama-C visitor for cumulative analyses: we add a few useful methods.

class type virtual ['a] cumulative_class = object .. end

module Make: functor (X : sig
val analysis_name : string
type t 

Type of the results




module T: Datatype.S  with type t = t
class virtual do_it : [t] Cumulative_analysis.cumulative_class

Class that implements the analysis.

end) -> sig .. end