sig
val are_comparable :
Cil_types.binop ->
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
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
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 ]
val maybe_warn_div : with_alarms:CilE.warn_mode -> Cvalue.V.t -> unit
val maybe_warn_indeterminate :
with_alarms:CilE.warn_mode -> Cvalue.V_Or_Uninitialized.t -> bool
val maybe_warn_completely_indeterminate :
with_alarms:CilE.warn_mode ->
Locations.location -> Cvalue.V_Or_Uninitialized.t -> Cvalue.V.t -> unit
val warn_top : unit -> 'a
end