module Value_messages: sig
.. end
UNDOCUMENTED.
type
warning =
Warnings can either emit ACSL (Alarm), or do not emit ACSL
(others).
type
value_message =
type
precision_loss_message =
| |
Exhausted_slevel |
| |
Garbled_mix_creation of Cil_types.exp |
| |
Garbled_mix_propagation |
type
callstack = unit
Temporary: avoid a circular dependency while CilE is used.
type
state = unit
module Value_Message_Callback: Hook.Build
(
sig
end
)
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