Module Value_messages

module Value_messages: sig .. end

type warning = 
| Alarm of Alarms.t * Property_status.emitted_status
| Bad_function_pointer
type value_message = 
| Warning of warning
| Property_evaluated of Property.t * Property_status.emitted_status
| Precision_Loss of precision_loss_message
| Feedback of unit
type precision_loss_message = 
| Exhausted_slevel
| Garbled_mix_creation of Cil_types.exp
| Garbled_mix_propagation
type callstack = unit 
type state = unit 
module Value_Message_Callback: Hook.Build(sig
type t = Value_messages.value_message * Cil_types.kinstr * Value_messages.callstack *
Value_messages.state
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