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-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

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

Module `Inout.Cumulative_analysis`Source

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).

Sourceval fold_implicit_initializer : Frama_c_kernel.Cil_types.typ -> bool

Should implicit zero-initializers for typ be folded? False for big arrays to avoid a performance issue.

Source

val specialize_state_on_call : 
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cvalue.Model.t

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

Sourceclass virtual 'a cumulative_visitor : object ... end

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

Sourceclass type virtual 'a cumulative_class = object ... end

Sourcemodule Make (X : sig ... end) : sig ... end