Module Value_messages

module Value_messages: sig .. end
UNDOCUMENTED.

type warning = 
| Alarm of Alarms.t * Cil_types.code_annotation * Property_status.emitted_status
| Bad_function_pointer
| Uncategorized of string
Warnings can either emit ACSL (Alarm), or do not emit ACSL (others).
type value_message = 
| Warning of warning
| Property_evaluated of Property.t * Property_status.emitted_status
| Precision_Loss of precision_loss_message
| Lattice_message of Lattice_messages.emitter * Lattice_messages.t
| Feedback of unit
type precision_loss_message = 
| Exhausted_slevel
| Garbled_mix_creation of Cil_types.exp
| Garbled_mix_propagation
type callstack = Value_types.callstack 
type state = Cvalue.Model.t 
module Value_Message_Callback: sig .. end
val curstate : (state * Trace.t) Pervasives.ref
val set_current_state : state * Trace.t -> unit
val ki_of_callstack : ('a * Cil_types.kinstr) list -> Cil_types.kinstr
module Alarm_key: Datatype.Pair_with_collections(Cil_datatype.Kinstr)(Alarms)(sig
val module_name : string
end)
module Alarm_cache: State_builder.Hashtbl(Alarm_key.Hashtbl)(Datatype.Unit)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val default_alarm_report : Cil_datatype.Kinstr.t ->
Alarms.t -> string -> Alarm_cache.data
val new_alarm : Cil_datatype.Kinstr.t ->
Alarms.t ->
Property_status.emitted_status ->
Cil_types.code_annotation ->
string -> Value_Message_Callback.result
val new_status : Property.t ->
Property_status.emitted_status ->
state * Trace.t ->
Value_Message_Callback.result
val warning : ('a, Format.formatter, unit, Value_Message_Callback.result)
Pervasives.format4 -> 'a