module Warn: sig
.. end
Alarms and imprecision warnings emitted during the analysis.
val are_comparable : Abstract_interp.Comp.t ->
Locations.Location_Bytes.t -> Locations.Location_Bytes.t -> bool
val check_no_recursive_call : Cil_types.kernel_function -> bool
val warn_modified_result_loc : with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Locations.location -> Cvalue.Model.t -> Cil_types.lval -> unit
This function should be used to treat a call lv = kf(...)
.
warn_modified_result_loc alarms loc state lv
checks that evaluating lv
in state
results in location
. If it is not the case, a warning about
a modification of lv
during the call to kf
is emitted
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_locals_escape_result : Cil_types.fundec -> 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_overlap : with_alarms:CilE.warn_mode ->
Cil_types.lval * Locations.location ->
Cil_types.lval * Locations.location -> unit
val warn_float : with_alarms:CilE.warn_mode ->
?non_finite:bool ->
?addr:bool -> Cil_types.fkind option -> (Format.formatter -> unit) -> unit
val warn_float_addr : with_alarms:CilE.warn_mode -> (Format.formatter -> unit) -> unit
val offsetmap_contains_imprecision : Cvalue.V_Offsetmap.t -> Cvalue.V.t option
Returns the first eventual imprecise part contained in an offsetmap
val warn_reduce_indeterminate_offsetmap : with_alarms:CilE.warn_mode ->
Cil_types.typ ->
Cvalue.V_Offsetmap.t ->
[ `Loc of Locations.location
| `NoLoc
| `PreciseLoc of Precise_locs.precise_location ] ->
Cvalue.Model.t -> [ `Bottom | `Res of Cvalue.V_Offsetmap.t * Cvalue.Model.t ]
If the supplied offsetmap has an arithmetic type and contains indeterminate
bits (uninitialized, or escaping address), raises the corresponding alarm(s)
and returns the reduced offsetmap and state. The location is the original
source of the offsetmap, and is used to reduce state
.
The syntactic context must have been positioned by the caller. If
some bits are guaranteed to be indeterminate, returns `Bottom
; this
indicates completely erroneous code.
val maybe_warn_div : with_alarms:CilE.warn_mode -> Cvalue.V.t -> unit
Emit an alarm about a non-null divisor when the supplied value may
contain zero.
val maybe_warn_indeterminate : with_alarms:CilE.warn_mode -> Cvalue.V_Or_Uninitialized.t -> bool
Warn for unitialized or escaping bits in the value passed
as argument. Returns true
when an alarm has been raised
val maybe_warn_completely_indeterminate : with_alarms:CilE.warn_mode ->
Locations.location -> Cvalue.V_Or_Uninitialized.t -> Cvalue.V.t -> unit
Print a message about the given location containing a completely
indeterminate value.
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.)