package frama-c

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

Frama-C visitor for cumulative analyses: we add a few useful methods. The method compute_kf must be used to add the effects of a call to the given kernel function to the pool of results

inherit Frama_c_kernel.Visitor.frama_c_inplace

If the current statement is a call to the given function, enrich the superposed memory state at this statement with the formal arguments of this function. Useful to do an analysis with a limited amount of context

method virtual compute_kf : Frama_c_kernel.Cil_types.kernel_function -> 'a

Virtual function to use when one needs to compute the effect of a function call. This function carries implicitly a context: thus calling self#compute_kf k1; self#compute_kf k2 is different from calling one within the other