Module Warn

module Warn: sig .. end
Alarms and imprecision warnings emitted during the analysis.

val warn_div : CilE.warn_mode -> addresses:bool -> unit
division. If addresses holds, also emit an alarm about the denominator not being comparable to \null.
val warn_shift : CilE.warn_mode -> unit
val warn_integer_overflow : CilE.warn_mode -> unit
val warn_float_to_int_overflow : CilE.warn_mode -> unit
val warn_pointer_subtraction : CilE.warn_mode -> unit
val warn_pointer_comparison : Cil_types.typ -> CilE.warn_mode -> unit
warn on invalid pointer comparison. The first argument is the type of the arguments of the comparison
val warn_nan_infinite : CilE.warn_mode -> unit
val warn_uninitialized : CilE.warn_mode -> unit
val warn_escapingaddr : CilE.warn_mode -> unit
val warn_mem : CilE.warn_mode -> unit
val warn_imprecise_lval_read : with_alarms:CilE.warn_mode ->
Cil_types.lval -> Locations.location -> Locations.Location_Bytes.t -> unit
val warn_locals_escape : bool -> Cil_types.fundec -> Base.t -> Base.SetLattice.t -> unit
val warn_right_exp_imprecision : with_alarms:CilE.warn_mode ->
Cil_types.lval -> Locations.location -> Cvalue.V.t -> unit
val warn_float : with_alarms:CilE.warn_mode -> ?non_finite:bool -> ?addr:bool -> unit -> unit
val warn_top : unit -> 'a
Abort the analysis, signaling that Top has been found. (Should not actually appear. No operation should produce Top, or those operations should be abstracted unsoundly.)