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-30.0-Zinc.tar.gz

sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56

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.

Source

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)

Sourceval compute_kf : WpContext.model -> Frama_c_kernel.Kernel_function.t -> unit

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

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