Module Valarms

module Valarms: sig .. end

Auxiliary function that displays two simultaneous alarms as a conjunction

division. If addresses holds, also emit an alarm about the denominator not being comparable to \null.

type syntactic_context =

`\|`	`SyNone`
`\|`	`SyCallResult`
`\|`	`SyBinOp of Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp`
`\|`	`SyUnOp of Cil_types.exp`
`\|`	`SyMem of Cil_types.lval`
`\|`	`SyMemLogic of Cil_types.term`
`\|`	`SySep of Cil_types.lval * Cil_types.lval`

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

division. If 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

Auxiliary function that displays two simultaneous alarms as a conjunction

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

warning to be emitted when two incompatible accesses to a location are done in unspecified order. Must be called in a SyNone or SySep context.

val warn_separated : CilE.warn_mode -> unit

val warn_overlap : (Format.formatter -> unit) -> CilE.warn_mode -> unit