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