Module Rte
module Rte: sig
.. end
type ('a, 'b)
alarm_gen = remove_trivial:bool ->
warning:bool -> Cil_types.kernel_function -> Cil_types.kinstr -> 'a -> 'b
val lval_assertion : read_only:Alarms.access_kind -> (Cil_types.lval, unit) alarm_gen
val divmod_assertion : (Cil_types.exp, unit) alarm_gen
val signed_div_assertion : (Cil_types.exp * Cil_types.exp * Cil_types.exp, unit) alarm_gen
val shift_alarm : (Cil_types.exp * int option, unit) alarm_gen
val signed_shift_assertion : (Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp, unit)
alarm_gen
val mult_sub_add_assertion : (bool * Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp,
unit)
alarm_gen
val uminus_assertion : (Cil_types.exp, unit) alarm_gen
val signed_downcast_assertion : (Cil_types.typ * Cil_types.exp, bool) alarm_gen
val unsigned_downcast_assertion : (Cil_types.typ * Cil_types.exp, bool) alarm_gen
val float_to_int_assertion : (Cil_types.typ * Cil_types.exp, bool) alarm_gen
val generated_annotations : unit -> Cil_types.code_annotation list
val reset_generated_annotations : unit -> unit
val save_alarms : bool Pervasives.ref