module Value_messages:sig
..end
type
warning =
| |
Alarm of |
| |
Bad_function_pointer |
type
value_message =
| |
Warning of |
| |
Property_evaluated of |
| |
Precision_Loss of |
| |
Feedback of |
type
precision_loss_message =
| |
Exhausted_slevel |
| |
Garbled_mix_creation of |
| |
Garbled_mix_propagation |
typecallstack =
unit
typestate =
unit
module Value_Message_Callback:Hook.Build
(
sig
typet =
Value_messages.value_message * Cil_types.kinstr * Value_messages.callstack *
Value_messages.stateend
)
val new_alarm : Cil_types.kinstr ->
Alarms.t ->
Property_status.emitted_status ->
Value_Message_Callback.result
val new_status : Property.t ->
Property_status.emitted_status ->
'a -> Value_Message_Callback.result