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 -> ?fct:Wp_parameters.functions -> ?bhv:string list -> ?prop:string list -> unit -> unit

Compute the entire set, populating specification related to:

  • exits
  • terminates
  • assigns (for functions without body)

Compute the target properties associated to the given kernel function. It also populates exits, terminates and assigns for the function and its callees, as well as RTE assertions if they are asked on command line.

  • since 28.0-Nickel
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 OCaml Planet 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