package frama-c

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

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.

val compute : WpContext.model -> unit
val iter : (Frama_c_kernel.Kernel_function.t -> unit) -> unit
  • 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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct