Module Value_messages

module Value_messages: sig .. end

UNDOCUMENTED.

type warning =

`\|`	`Alarm of Alarms.t * Property_status.emitted_status`
`\|`	`Bad_function_pointer`

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`
`\|`	`Feedback of unit`

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
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