package frama-c

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

Value analysis alarms

type alarm_behavior = unit -> unit
val a_ignore : alarm_behavior
type warn_mode = {
  1. defined_logic : alarm_behavior;
    (*

    operations that raise an error only in the C, not in the logic

    *)
  2. unspecified : alarm_behavior;
    (*

    defined but unspecified behaviors

    *)
  3. 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.

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