module CilE: sig
.. end
type
syntactic_context =
val start_stmt : Cil_types.kinstr -> unit
val end_stmt : unit -> unit
val current_stmt : unit -> Cil_types.kinstr
val set_syntactic_context : syntactic_context -> unit
val get_syntactic_context : unit -> Cil_types.kinstr * syntactic_context
type
alarm_behavior = {
}
val do_warn : alarm_behavior ->
(Emitter.t * (Format.formatter -> unit) -> unit) -> unit
val a_ignore : alarm_behavior
type
warn_mode = {
}
An argument of type
warn_mode
is required by some of the access
functions in
Db.Value
(the interface to the value analysis). This
argument tells what should be done with the various messages
that the value analysis emits during the call.
Each warn_mode
field indicates the expected treatment for one
category of message. These fields are not completely fixed
yet. However, you can still used functions CilE.warn_all_mode
and
CilE.warn_none_mode
below when you have to provide an argument of type
warn_mode
.
val warn_all_mode : Emitter.t -> (Format.formatter -> unit) -> warn_mode
Emit all messages, including alarms and informative messages
regarding the loss of precision.
val warn_none_mode : warn_mode
Do not emit any message.
val warn_div : warn_mode -> unit
val warn_shift : warn_mode -> int -> unit
val warn_shift_left_positive : warn_mode -> unit
val warn_mem_read : warn_mode -> unit
val warn_mem_write : warn_mode -> unit
val warn_integer_overflow : warn_mode ->
signed:bool -> min:Integer.t option -> max:Integer.t option -> unit
val warn_float_to_int_overflow : warn_mode ->
Integer.t option -> Integer.t option -> (Format.formatter -> unit) -> unit
val warn_index : warn_mode -> positive:bool -> range:string -> unit
warn_index w ~positive ~range
emits a warning signaling an out of bounds
access. The expression used as index is taken from the syntactic context.
range
is used to display the inferred values for the index.
If positive
is true, the generated assertion is of the form
e < upper_bound
; otherwise, two assertions are generated: 0 <= e
and e < upper_bound
.
val warn_pointer_comparison : warn_mode -> unit
val warn_valid_string : warn_mode -> unit
val warn_pointer_subtraction : warn_mode -> unit
val warn_nan_infinite : warn_mode ->
Cil_types.fkind option -> (Format.formatter -> unit) -> unit
val warn_uninitialized : warn_mode -> unit
val warn_escapingaddr : warn_mode -> unit
warning to be emitted when two incompatible accesses to a location are
done in unspecified order. Must be called in a SyNone
or SySep
context.
val warn_separated : warn_mode -> unit
val warn_overlap : Locations.location * Locations.location -> warn_mode -> unit