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