module CilE:sig
..end
type
alarm_behavior = {
|
a_log : |
(* |
should the alarm be sent to the log
| *) |
|
a_call : |
(* |
call function after optionally emitting with field a_log.
| *) |
val a_ignore : alarm_behavior
type
warn_mode = {
|
imprecision_tracing : |
(* |
informative messages for garbled values
| *) |
|
defined_logic : |
(* |
operations that raise an error only in the C, not in the logic
| *) |
|
unspecified : |
(* |
defined but unspecified behaviors
| *) |
|
others : |
(* |
all the remaining undefined behaviors
| *) |
warn_mode
is required by some of the access
functions in Db.Value
(the interface to the value analysis). This
argument tells what should be done with the various messages
that the value analysis emits during the call.
Each warn_mode
field indicates the expected treatment for one
category of message. These fields are not completely fixed
yet. However, you can still used functions CilE.warn_all_mode
and
CilE.warn_none_mode
below when you have to provide an argument of type
warn_mode
.
val warn_all_mode : warn_mode
val warn_none_mode : warn_mode