package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c-inout.core/Inout/Cumulative_analysis/class-cumulative_visitor/index.html

Class `Cumulative_analysis.cumulative_visitor`Source

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

method specialize_state_on_call : Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cvalue.Model.t

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