module Rte:sig
..end
type'a
alarm_gen =remove_trivial:bool ->
on_alarm:(invalid:bool -> Alarms.alarm -> unit) -> 'a -> unit
'a alarm_gen
is an abstraction over the process of generating a certain
kind of RTEs over something of type 'a
.
The on_alarm
argument receives all corresponding alarms, with
optionally a status indicating that the alarm is red.
val lval_assertion : read_only:Alarms.access_kind -> Cil_types.lval alarm_gen
val lval_initialized_assertion : Cil_types.lval alarm_gen
val divmod_assertion : Cil_types.exp alarm_gen
val signed_div_assertion : (Cil_types.exp * Cil_types.exp * Cil_types.exp) alarm_gen
val shift_width_assertion : (Cil_types.exp * Cil_types.typ) alarm_gen
val shift_negative_assertion : Cil_types.exp alarm_gen
val shift_overflow_assertion : signed:bool ->
(Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp)
alarm_gen
val mult_sub_add_assertion : signed:bool ->
(Cil_types.exp * Cil_types.binop * Cil_types.exp * Cil_types.exp)
alarm_gen
val uminus_assertion : Cil_types.exp alarm_gen
val downcast_assertion : (Cil_types.typ * Cil_types.exp) alarm_gen
val float_to_int_assertion : (Cil_types.typ * Cil_types.exp) alarm_gen
val finite_float_assertion : (Cil_types.fkind * Cil_types.exp) alarm_gen
val pointer_call : (Cil_types.exp * Cil_types.exp list) alarm_gen
val pointer_value : Cil_types.exp alarm_gen
val bool_value : Cil_types.lval alarm_gen