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 -> Cvalue.V.t -> 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_indeterminate_offsetmap : with_alarms:CilE.warn_mode ->
Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.t option
None
; this indicates
completely erroneous code.val warn_float_addr : with_alarms:CilE.warn_mode -> (Format.formatter -> unit) -> unit
val warn_float : with_alarms:CilE.warn_mode ->
?overflow:bool ->
?addr:bool -> Cil_types.fkind option -> (Format.formatter -> unit) -> unit