module Valarms:sig
..end
division. If addresses
holds, also emit an alarm about the denominator
not being comparable to \null.
type
syntactic_context =
| |
SyNone |
| |
SyCallResult |
| |
SyBinOp of |
| |
SyUnOp of |
| |
SyMem of |
| |
SyMemLogic of |
| |
SySep of |
val local_printer : Printer.extensible_printer
val current_stmt_tbl : Cil_datatype.Kinstr.t Stack.t
val start_stmt : Cil_datatype.Kinstr.t -> unit
val end_stmt : unit -> unit
val current_stmt : unit -> Cil_datatype.Kinstr.t
val syntactic_context : syntactic_context Pervasives.ref
val set_syntactic_context : syntactic_context -> unit
val get_syntactic_context : unit -> Cil_datatype.Kinstr.t * syntactic_context
val sc_kinstr_loc : Cil_types.kinstr -> Cil.CurrentLoc.data
val do_warn : CilE.alarm_behavior ->
(Emitter.t * (Format.formatter -> unit) -> unit) -> unit
val register_alarm : ?kf:Cil_types.kernel_function ->
?status:Property_status.emitted_status ->
Emitter.t -> Cil_types.kinstr -> Alarms.t -> Cil_types.code_annotation * bool
val warn_pointer_comparison : CilE.warn_mode -> unit
val warn_div : CilE.warn_mode -> addresses:bool -> unit
addresses
holds, also emit an alarm about the denominator
not being comparable to \null.val warn_conjuctive_annots : (Cil_types.code_annotation -> unit) ->
Cil_types.code_annotation option -> Cil_types.code_annotation option -> unit
val warn_integer_overflow : CilE.warn_mode ->
signed:bool -> min:Integer.t option -> max:Integer.t option -> unit
val warn_float_to_int_overflow : CilE.warn_mode ->
Integer.t option -> Integer.t option -> (Format.formatter -> unit) -> unit
val warn_shift : CilE.warn_mode -> int -> unit
val warn_shift_left_positive : CilE.warn_mode -> unit
val pretty_warn_mem_mode : Format.formatter -> Alarms.access_kind -> unit
val warn_mem : CilE.warn_mode -> Alarms.access_kind -> unit
val warn_mem_read : CilE.warn_mode -> unit
val warn_mem_write : CilE.warn_mode -> unit
val warn_index : CilE.warn_mode -> positive:bool -> range:string -> unit
warn_index w ~positive ~range
emits a warning signaling an out of bounds
access. The expression used as index is taken from the syntactic context.
range
is used to display the inferred values for the index.
If positive
is true, the generated assertion is of the form
e < upper_bound
; otherwise, two assertions are generated: 0 <= e
and e < upper_bound
.val warn_valid_string : CilE.warn_mode -> unit
val warn_pointer_subtraction : CilE.warn_mode -> unit
val warn_nan_infinite : CilE.warn_mode ->
Cil_types.fkind option -> (Format.formatter -> unit) -> unit
val warn_uninitialized : CilE.warn_mode -> unit
val warn_escapingaddr : CilE.warn_mode -> unit
SyNone
or SySep
context.val warn_separated : CilE.warn_mode -> unit
val warn_overlap : (Format.formatter -> unit) -> CilE.warn_mode -> unit