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-wp.core/Wp/WpTarget/index.html

Module `Wp.WpTarget`Source

This module computes the set of kernel functions that are considered by the command line options transmitted to WP. That is:

all functions on which a verification must be tried,
all functions that are called by the previous ones,
including those parameterized via the 'calls' clause.

It takes in account the options -wp-bhv and -wp-props so that if all functions are initially selected but in fact some of them are filtered out by these options, they are not considered.

Sourceval compute : WpContext.model -> unit

Sourceval iter : (Frama_c_kernel.Kernel_function.t -> unit) -> unit

Source

val with_callees : 
  Frama_c_kernel.Kernel_function.t ->
  Frama_c_kernel.Kernel_function.Set.t

returns
the set composed of the given kernel_function together with its callees. If this function does not have a definition, the empty set is returned.