Module Warn

module Warn: sig .. end
Check that 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
Check that kf is not already present in the call stack
val warn_modified_result_loc : with_alarms:CilE.warn_mode ->
Kernel_function.t ->
Locations.Location.t -> Db.Value.state -> 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_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
Returns the first eventual imprecise part contained in an offsetmap
val warn_indeterminate_offsetmap : with_alarms:CilE.warn_mode ->
Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.t option
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. The syntactic context must have been positioned by the caller. If some bits are guaranteed to be indeterminate, returns 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