Module Frama_c_kernel.CilE

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.