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.kernel/Frama_c_kernel/CilE/index.html

Module `Frama_c_kernel.CilE`

Value analysis alarms

type alarm_behavior = unit -> unit

val a_ignore : alarm_behavior

type warn_mode = {

defined_logic : alarm_behavior;
(*
operations that raise an error only in the C, not in the logic
*)
unspecified : alarm_behavior;
(*
defined but unspecified behaviors
*)
others : alarm_behavior;
(*
all the remaining undefined behaviors
*)

}

An argument of type warn_mode can be supplied to some of the access functions in Db.Value (the interface to the value analysis). Each field of warn_mode indicates the action to perform for each category of alarm. These fields are not completely fixed yet. However, you can use the value warn_none_mode below when you have to provide an argument of type warn_mode.

val warn_none_mode : warn_mode

Do not emit any message.