module Warn:sig
..end
kf
is not already present in the call stack
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
exception Distinguishable_strings
val check_not_comparable : Cil_types.binop ->
Locations.Location_Bytes.t -> Locations.Location_Bytes.t -> bool
exception Recursive_call
val check_no_recursive_call : Kernel_function.t -> bool
kf
is not already present in the call stackval warn_modified_result_loc : with_alarms:CilE.warn_mode ->
Kernel_function.t ->
Locations.Location.t -> Db.Value.state -> Cil_types.lval -> unit
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 emittedval 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_imprecise_lval_read : with_alarms:CilE.warn_mode ->
Cil_types.lval -> Locations.location -> Locations.Location_Bytes.z -> unit
val warn_right_exp_imprecision : with_alarms:CilE.warn_mode ->
Cil_types.lval -> Locations.location -> Locations.Location_Bytes.z -> unit
val warn_overlap : with_alarms:CilE.warn_mode ->
Cil_types.lval * Locations.location ->
Cil_types.lval * Locations.location -> unit
exception Got_imprecise of Cvalue.V.t
val offsetmap_contains_imprecision : Cvalue.V_Offsetmap.t -> Cvalue.V.t option
val warn_reduce_indeterminate_offsetmap : with_alarms:CilE.warn_mode ->
Cil_types.typ ->
Cvalue.Model.offsetmap ->
[< `Loc of Locations.location
| `NoLoc
| `PreciseLoc of Precise_locs.precise_location ] ->
Cvalue.Model.t ->
[> `Bottom | `Res of Cvalue.Model.offsetmap * Cvalue.Model.t ]
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_indeterminate : with_alarms:CilE.warn_mode -> Cvalue.V_Or_Uninitialized.un_t -> bool
true
when an alarm has been raisedval maybe_warn_completely_indeterminate : with_alarms:CilE.warn_mode ->
Locations.location -> Cvalue.V_Or_Uninitialized.t -> Cvalue.V.t -> unit
val warn_float_addr : with_alarms:CilE.warn_mode -> (Format.formatter -> unit) -> unit
val warn_float : with_alarms:CilE.warn_mode ->
?non_finite:bool ->
?addr:bool -> Cil_types.fkind option -> (Format.formatter -> unit) -> unit
val maybe_warn_div : with_alarms:CilE.warn_mode -> Cvalue.V.t -> unit
val warn_top : unit -> 'a