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 annotations : Cil_types.code_annotation list Pervasives.ref
val generated_annotations : unit -> Cil_types.code_annotation list
val reset_generated_annotations : unit -> unit
val save_alarms : bool Pervasives.ref
val register_alarm : Emitter.t ->
Cil_types.kernel_function ->
Cil_types.kinstr ->
?status:Property_status.emitted_status ->
Alarms.alarm -> Cil_types.code_annotation
val local_printer : Printer.extensible_printer
val get_expr_val : Cil_types.exp -> Integer.t option
val valid_index : remove_trivial:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.exp -> Cil_types.exp -> unit
val lval_assertion : read_only:Alarms.access_kind ->
remove_trivial:bool ->
warning:'a ->
Cil_types.kernel_function -> Cil_types.kinstr -> Cil_types.lval -> unit
val uminus_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function -> Cil_types.kinstr -> Cil_types.exp -> unit
val mult_sub_add_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr ->
bool * Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp ->
unit
val divmod_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function -> Cil_types.kinstr -> Cil_types.exp -> unit
val signed_div_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.exp * Cil_types.exp * Cil_types.exp -> unit
val shift_alarm : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.exp * int option -> unit
val signed_shift_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp -> unit
val unsigned_downcast_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.typ * Cil_types.exp -> bool
val signed_downcast_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.typ * Cil_types.exp -> bool
val float_to_int_assertion : remove_trivial:bool ->
warning:bool ->
Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.typ * Cil_types.exp -> bool