package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Class that implements the analysis. Must not deal with memoization, as this is automatically done by the functor

inherit 'a cumulative_visitor
method bottom : 'a
method result : 'a

Result of the analysis

method join : 'a -> unit

Adding partial results to the current ones

method compute_funspec : Frama_c_kernel.Cil_types.kernel_function -> 'a

Function that computes and returns the partial results on a funspec. May consult self#current_stmt to specialize itself, and return partially contextual results

method clean_kf_result : Frama_c_kernel.Cil_types.kernel_function -> 'a -> 'a

Assuming v are the results of the analysis for f (ie. the union of the results on all the statements of f, or compute_funspec f if f has no body), clean_kf_result k v cleans those results before storing them. Use for example to remove out-of-scope locals