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 -> 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
Returns the first eventual imprecise part contained in an offsetmap
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 ]
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_indeterminate : with_alarms:CilE.warn_mode -> Cvalue.V_Or_Uninitialized.un_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_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
Emit an alarm about a non-null divisor when the supplied value may contain zero.
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.)