diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index 7c7ef14725bda19ec818b27f47060fddfd1d40f7..fb3e32553ca4014f94426d46d9103522c87a7766 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -22,13 +22,42 @@
(** Some functions are also registered in {!Db.Value}. *)
-open Cil_types
-
+(* --- included from visit.mli --- *)
module Visit :
sig
- (** Low-level control over iterators *)
+ open Cil_types
+
+ (** {2 RTE Generator API}
+
+ The all-in-one entry points of the RTE plugin.
+ *)
+
+ (** Generates RTE for a single function. Uses the status of the various
+ RTE options do decide which kinds of annotations must be generated.
+ *)
+ val annotate_kf: kernel_function -> unit
+
+ (** Generates all RTEs for a given function. *)
+ val do_all_rte: kernel_function -> unit
+
+ (** Generates all RTEs except preconditions for a given function. *)
+ val do_rte: kernel_function -> unit
+
+ val rte_annotations: stmt -> code_annotation list
+ val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
+ val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
+
+ (** Main entry point of the plug-in, used by [-rte] option: computes
+ RTE on the whole AST. Which kind of RTE is generated depends on the
+ options given on the command line.
+ *)
+ val compute: unit -> unit
+
+ (** {2 Low Level Iterator Control} *)
+ (** Flags for controling the low-level API. Each flag control whether
+ a category of alarms will be visited or not. *)
type flags = {
remove_trivial: bool;
initialized: bool;
@@ -47,7 +76,7 @@ sig
bool_value: bool;
}
- (** Defaults are taken from the Kernel and RTE plug-in options *)
+ (** Defaults flags are taken from the Kernel and RTE plug-in options. *)
val default :
?remove_trivial:bool ->
?initialized:bool ->
@@ -66,21 +95,34 @@ sig
?bool_value:bool ->
unit -> flags
- (** All flags set to [true] *)
+ (** All flags set to [true]. *)
val flags_all : flags
- (** All flags set to [false] *)
+ (** All flags set to [false]. *)
val flags_none : flags
- (** Low-level iterators callback.
+ (** {2 Low-Level RTE Iterators}
+
+ RTE Iterators allow to traverse a Cil AST fragment (stmt, expr, l-value)
+ and reveal its potential Alarms. Each alarm will be presented to a callback
+ with type [on_alarm], that you can use in turn to generate an annotation
+ or perform any other treatment.
+
+ Flags can be used to select which alarm categories to visit, with
+ defaults derived from Kernel and RTE plug-in parameters.
+ *)
+
+ (** Alarm callback.
+
+ The [on_alarm kf stmt ~invalid alarm] callback is invoked on each
+ alarm visited by an RTE iterator, provided it fits the selected categories.
+ The [kf] and [stmt] designates the statement originating the alarm,
+ while [~invalid:true] is set when the alarm trivially evaluates to false.
+ In this later case, the corresponding annotation shall be assigned
+ the status [False_if_reachable].
- The [on_alarm stmt ?status alarm] callback is invoked with
- the [stmt] originating the alarm and the already known status,
- if any.
*)
- type on_alarm =
- kinstr -> ?status:Property_status.emitted_status ->
- Alarms.alarm -> unit
+ type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
(** Low-level iterators
@@ -94,13 +136,33 @@ sig
type 'a iterator =
?flags:flags -> on_alarm ->
- Kernel_function.t ->
- Cil_types.stmt ->
- 'a -> unit
+ Kernel_function.t -> Cil_types.stmt -> 'a -> unit
val iter_lval : lval iterator
val iter_exp : exp iterator
val iter_instr : instr iterator
val iter_stmt : stmt iterator
+ (** {2 Alarm Helpers} *)
+
+ (** Returns a [False_if_reachable] status when invalid. *)
+ val status : invalid:bool -> Property_status.emitted_status option
+
+ (** Registers and returns the annotation associated with the alarm,
+ and a boolean flag indicating whether it has been freshly generated
+ or not. *)
+ val annotation :
+ Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
+ code_annotation * bool
+
+ (** A callback that simply register the annotation associated with the alarm. *)
+ val register : Emitter.t -> on_alarm
+
+(*
+Local Variables:
+compile-command: "make -C ../../.."
+End:
+*)
+
+
end
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 130ec5506858bfa9a07a75eb8687dc99e86a730f..b1f2b7ffaec2b3a980a1816314f0756e902e471e 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -24,9 +24,7 @@ open Cil_types
type 'a alarm_gen =
remove_trivial:bool ->
- on_alarm:(?status:Property_status.emitted_status ->
- Alarms.alarm ->
- unit) ->
+ on_alarm:(invalid:bool -> Alarms.alarm -> unit) ->
'a -> unit
type bound_kind = Alarms.bound_kind = Lower_bound | Upper_bound
@@ -45,7 +43,7 @@ let valid_index ~remove_trivial ~on_alarm e size =
in
(* Do not create upper-bound check on GNU zero-length arrays *)
if not (bk == Upper_bound && Cil.isZero size) then begin
- on_alarm ?status:None (Alarms.Index_out_of_bound(e, b))
+ on_alarm ~invalid:false (Alarms.Index_out_of_bound(e, b))
end
in
if remove_trivial then begin
@@ -80,7 +78,7 @@ let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
match off with
| NoOffset ->
if default then
- on_alarm ?status:None (Alarms.Memory_access(lv, read_only))
+ on_alarm ~invalid:false (Alarms.Memory_access(lv, read_only))
| Field (fi, off) ->
(* Mark that we went through a struct field, then recurse *)
check_array_access default off fi.ftype true
@@ -124,10 +122,10 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
cfields
in
if default then
- on_alarm ?status:None (Alarms.Uninitialized_union llv))
+ on_alarm ~invalid:false (Alarms.Uninitialized_union llv))
| _ ->
if default then
- on_alarm ?status:None (Alarms.Uninitialized lv)
+ on_alarm ~invalid:false (Alarms.Uninitialized lv)
end
| Field (fi, off) ->
(* Mark that we went through a struct field, then recurse *)
@@ -158,9 +156,9 @@ let uminus_assertion ~remove_trivial ~on_alarm exp =
let min_ty = Cil.min_signed_number size in
(* alarm is bound <= exp, hence bound must be MIN_INT+1 *)
let bound = Integer.add Integer.one min_ty in
- let alarm ?status () =
+ let alarm ?(invalid=false) () =
let a = Alarms.Overflow(Alarms.Signed, exp, bound, Lower_bound) in
- on_alarm ?status a
+ on_alarm ~invalid a
in
if remove_trivial then begin
match get_expr_val exp with
@@ -168,7 +166,7 @@ let uminus_assertion ~remove_trivial ~on_alarm exp =
| Some a64 ->
(* constant operand *)
if Integer.equal a64 min_ty then
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
end
else alarm ()
@@ -183,13 +181,13 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
if signed then Cil.min_signed_number size, Cil.max_signed_number size
else Integer.zero, Cil.max_unsigned_number size
in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let bound = match bk with
| Upper_bound -> max_ty
| Lower_bound -> min_ty
in
let signed = if signed then Alarms.Signed else Alarms.Unsigned in
- on_alarm ?status (Alarms.Overflow (signed, exp, bound, bk));
+ on_alarm ~invalid (Alarms.Overflow (signed, exp, bound, bk));
in
let alarms () =
alarm Lower_bound;
@@ -199,7 +197,7 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
match get_expr_val lexp, get_expr_val rexp, op with
| Some l, Some r, _ -> (* both operands are constant *)
let warn r =
- let warn bk = alarm ~status:Property_status.False_if_reachable bk in
+ let warn bk = alarm ~invalid:true bk in
if Integer.gt r max_ty then warn Upper_bound
else if Integer.lt r min_ty then warn Lower_bound
in
@@ -240,8 +238,8 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
(* assertions for division and modulo (divisor is 0) *)
let divmod_assertion ~remove_trivial ~on_alarm divisor =
(* division or modulo: overflow occurs when divisor is equal to zero *)
- let alarm ?status () =
- on_alarm ?status (Alarms.Division_by_zero divisor);
+ let alarm ?(invalid=false) () =
+ on_alarm ~invalid (Alarms.Division_by_zero divisor);
in
if remove_trivial then begin
match get_expr_val divisor with
@@ -250,7 +248,7 @@ let divmod_assertion ~remove_trivial ~on_alarm divisor =
| Some v64 ->
if Integer.equal v64 Integer.zero then
(* divide by 0 *)
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
(* else divide by constant which is not 0: nothing to assert *)
end
else alarm ()
@@ -270,9 +268,9 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
(* check dividend_expr / divisor_expr : if constants ... *)
(* compute smallest representable "size bits" (signed) integer *)
let max_ty = Cil.max_signed_number size in
- let alarm ?status () =
+ let alarm ?(invalid=false) () =
let a = Alarms.Overflow(Alarms.Signed, exp, max_ty, Alarms.Upper_bound) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
if remove_trivial then begin
let min = Cil.min_signed_number size in
@@ -285,7 +283,7 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
()
| Some _, Some _ ->
(* invalid constant division *)
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
| None, Some _ | Some _, None | None, None ->
(* at least one is not constant: cannot conclude *)
alarm ()
@@ -294,9 +292,9 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
(* Assertions for the left and right operands of left and right shift. *)
let shift_assertion ~remove_trivial ~on_alarm (exp, upper_bound) =
- let alarm ?status () =
+ let alarm ?(invalid=false) () =
let a = Alarms.Invalid_shift(exp, upper_bound) in
- on_alarm ?status a;
+ on_alarm ~invalid a ;
in
if remove_trivial then begin
match get_expr_val exp with
@@ -310,7 +308,7 @@ let shift_assertion ~remove_trivial ~on_alarm (exp, upper_bound) =
| Some u -> Integer.lt c64 (Integer.of_int u)
in
if not (Integer.ge c64 Integer.zero && upper_bound_ok) then
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
end
else alarm ()
@@ -340,10 +338,10 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
then Cil.max_signed_number size
else Cil.max_unsigned_number size
in
- let overflow_alarm ?status () =
+ let overflow_alarm ?(invalid=false) () =
let signed = if signed then Alarms.Signed else Alarms.Unsigned in
let a = Alarms.Overflow (signed, exp, maxValResult, Alarms.Upper_bound) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
if remove_trivial then begin
match get_expr_val lexp, get_expr_val rexp with
@@ -355,7 +353,7 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
if Integer.ge rval64 Integer.zero
&& Integer.gt (Integer.shift_left lval64 rval64) maxValResult
then
- overflow_alarm ~status:Property_status.False_if_reachable ()
+ overflow_alarm ~invalid:true ()
end
else overflow_alarm ()
@@ -375,13 +373,13 @@ let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
ok is same bit size ;
if target is <, requires <= max target *)
let max_ty = Cil.max_unsigned_number szTo in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> Integer.zero
| Upper_bound -> max_ty
in
let a = Alarms.Overflow (Alarms.Unsigned_downcast, exp, b, bk) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
let alarms () =
if Cil.isSigned kind then begin (* signed to unsigned *)
@@ -395,11 +393,9 @@ let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
| None -> alarms ()
| Some a64 ->
if Integer.lt a64 Integer.zero then
- alarm ~status:Property_status.False_if_reachable
- Lower_bound
+ alarm ~invalid:true Lower_bound
else if Integer.gt a64 max_ty then
- alarm ~status:Property_status.False_if_reachable
- Upper_bound
+ alarm ~invalid:true Upper_bound
end
else alarms ())
| _ -> ()
@@ -416,13 +412,13 @@ let signed_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
(* downcast: the expression result should fit on szTo bits *)
let min_ty = Cil.min_signed_number szTo in
let max_ty = Cil.max_signed_number szTo in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> min_ty
| Upper_bound -> max_ty
in
let a = Alarms.Overflow (Alarms.Signed_downcast, exp, b, bk) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
let alarms () =
if Cil.isSigned kind then begin
@@ -437,9 +433,9 @@ let signed_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
| None -> alarms ()
| Some a64 ->
(if Integer.lt a64 min_ty then
- alarm ~status:Property_status.False_if_reachable Lower_bound
+ alarm ~invalid:true Lower_bound
else if Integer.gt a64 max_ty then
- alarm ~status:Property_status.False_if_reachable Upper_bound)
+ alarm ~invalid:true Upper_bound)
end
else alarms ())
| _ -> ()
@@ -456,12 +452,12 @@ let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
else
Integer.zero, Cil.max_unsigned_number szTo
in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> min_ty
| Upper_bound -> max_ty
in
- on_alarm ?status (Alarms.Float_to_int (exp, b, bk))
+ on_alarm ~invalid (Alarms.Float_to_int (exp, b, bk))
in
let f = match exp.enode with
| Const (CReal (f, _, _)) -> Some f
@@ -474,9 +470,9 @@ let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
try
let fint = Floating_point.truncate_to_integer f in
if Integer.lt fint min_ty then
- alarm ~status:Property_status.False_if_reachable Lower_bound
+ alarm ~invalid:true Lower_bound
else if Integer.gt fint max_ty then
- alarm ~status:Property_status.False_if_reachable Upper_bound
+ alarm ~invalid:true Upper_bound
with Floating_point.Float_Non_representable_as_Int64 sign ->
match sign with
| Floating_point.Neg -> alarm Lower_bound
@@ -490,19 +486,19 @@ let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
(* assertion for checking only finite float are used *)
let finite_float_assertion ~remove_trivial:_ ~on_alarm (fkind, exp) =
- let status = None in
+ let invalid = false in
match Kernel.SpecialFloat.get () with
| "none" -> ()
- | "nan" -> on_alarm ?status (Alarms.Is_nan (exp, fkind))
- | "non-finite" -> on_alarm ?status (Alarms.Is_nan_or_infinite (exp, fkind))
+ | "nan" -> on_alarm ~invalid (Alarms.Is_nan (exp, fkind))
+ | "non-finite" -> on_alarm ~invalid (Alarms.Is_nan_or_infinite (exp, fkind))
| _ -> assert false
(* assertion for a pointer call [( *e )(args)]. *)
let pointer_call ~remove_trivial:_ ~on_alarm (e, args) =
- on_alarm ?status:None (Alarms.Function_pointer (e, Some args))
+ on_alarm ~invalid:false (Alarms.Function_pointer (e, Some args))
let bool_value ~remove_trivial:_ ~on_alarm lv =
- on_alarm ?status:None (Alarms.Invalid_bool lv)
+ on_alarm ~invalid:false (Alarms.Invalid_bool lv)
(*
Local Variables:
diff --git a/src/plugins/rte/rte.mli b/src/plugins/rte/rte.mli
index 0b1d55a21e304b9ccec0cb61b1c270fe232f69a9..6d194a63109c9b13466d45139ea283f3a8b18ee9 100644
--- a/src/plugins/rte/rte.mli
+++ b/src/plugins/rte/rte.mli
@@ -24,9 +24,7 @@ open Cil_types
type 'a alarm_gen =
remove_trivial:bool ->
- on_alarm:(?status:Property_status.emitted_status ->
- Alarms.alarm ->
- unit) ->
+ 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].
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index e262588f298b146e290004a6844ef6fb6d2ab2f4..dea0d52eeee985c6c0693ba1b6ac6231df4e5bf8 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -224,7 +224,8 @@ class annot_visitor kf flags on_alarm = object (self)
method private generate_assertion: 'a. 'a Rte.alarm_gen -> 'a -> unit =
fun fgen ->
- let on_alarm ?status a = on_alarm self#current_kinstr ?status a in
+ let stmt = Extlib.the (self#current_stmt) in
+ let on_alarm ~invalid a = on_alarm stmt ~invalid a in
fgen ~remove_trivial:flags.remove_trivial ~on_alarm
method! vstmt s = match s.skind with
@@ -464,31 +465,39 @@ let rte_annotations stmt =
(** {2 Iterate over Alarms on Cil elements} *)
-type on_alarm =
- kinstr -> ?status:Property_status.emitted_status ->
- Alarms.alarm -> unit
+type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
let iter_alarms visit ?flags (on_alarm:on_alarm) kf stmt element =
let flags = match flags with
| None -> default ()
| Some opt -> opt in
let visitor = object (self)
- inherit annot_visitor kf flags on_alarm
+ inherit annot_visitor kf flags (on_alarm kf)
initializer self#push_stmt stmt
end in
ignore (visit (visitor :> Cil.cilVisitor) element)
type 'a iterator =
?flags:flags -> on_alarm ->
- Kernel_function.t ->
- Cil_types.stmt ->
- 'a -> unit
+ Kernel_function.t -> Cil_types.stmt -> 'a -> unit
let iter_lval : lval iterator = iter_alarms Cil.visitCilLval
let iter_exp : exp iterator = iter_alarms Cil.visitCilExpr
let iter_instr : instr iterator = iter_alarms Cil.visitCilInstr
let iter_stmt : stmt iterator = iter_alarms Cil.visitCilStmt
+(** {2 Regitration} *)
+
+let status ~invalid =
+ if invalid then Some Property_status.False_if_reachable else None
+
+let annotation emitter kf stmt ~invalid alarm =
+ let status = status ~invalid in
+ Alarms.register emitter ~kf (Kstmt stmt) ?status alarm
+
+let register emitter kf stmt ~invalid alarm =
+ ignore (annotation emitter kf stmt ~invalid alarm)
+
(** {2 List of all RTEs on a given Cil object} *)
let get_annotations from kf stmt x =
@@ -496,8 +505,8 @@ let get_annotations from kf stmt x =
(* Accumulator containing all the code_annots corresponding to an alarm
emitted so far. *)
let code_annots = ref [] in
- let on_alarm ki ?status:_ alarm =
- let ca, _ = Alarms.to_annot ki alarm in
+ let on_alarm stmt ~invalid:_ alarm =
+ let ca, _ = Alarms.to_annot (Kstmt stmt) alarm in
code_annots := ca :: !code_annots;
in
let o = object (self)
@@ -512,7 +521,6 @@ let do_stmt_annotations kf stmt =
let do_exp_annotations = get_annotations Cil.visitCilExpr
-
(** {2 Annotations of kernel_functions for a given type of RTE} *)
(* generates annotation for function kf on the basis of [flags] *)
@@ -552,13 +560,11 @@ let annotate_kf_aux flags kf =
then begin
Options.feedback "annotating function %a" Kernel_function.pretty kf;
let warn = Options.Warn.get () in
- let on_alarm ki ?status alarm =
- let ca, _ = Alarms.register Generator.emitter ~kf ki ?status alarm in
- match warn, status with
- | true, Some Property_status.False_if_reachable ->
+ let on_alarm stmt ~invalid alarm =
+ let ca, _ = annotation Generator.emitter kf stmt ~invalid alarm in
+ if warn && invalid then
Options.warn "@[guaranteed RTE:@ %a@]"
Printer.pp_code_annotation ca
- | _ -> ()
in
let vis = new annot_visitor kf flags on_alarm in
let nkf = Visitor.visitFramacFunction vis f in
diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli
index 3aab4626ecfd71cd4cc205de37bea8e01a030ada..4c7f5fc71030ec45ed203a5f00936d146994f052 100644
--- a/src/plugins/rte/visit.mli
+++ b/src/plugins/rte/visit.mli
@@ -20,10 +20,40 @@
(* *)
(**************************************************************************)
+(* --- Synchronized with RteGen.mli --- *)
+
open Cil_types
-(** Low-level control over iterators *)
+(** {2 RTE Generator API}
+
+ The all-in-one entry points of the RTE plugin.
+*)
+
+(** Generates RTE for a single function. Uses the status of the various
+ RTE options do decide which kinds of annotations must be generated.
+*)
+val annotate_kf: kernel_function -> unit
+
+(** Generates all RTEs for a given function. *)
+val do_all_rte: kernel_function -> unit
+
+(** Generates all RTEs except preconditions for a given function. *)
+val do_rte: kernel_function -> unit
+
+val rte_annotations: stmt -> code_annotation list
+val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
+val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
+
+(** Main entry point of the plug-in, used by [-rte] option: computes
+ RTE on the whole AST. Which kind of RTE is generated depends on the
+ options given on the command line.
+*)
+val compute: unit -> unit
+
+(** {2 Low Level Iterator Control} *)
+(** Flags for controling the low-level API. Each flag control whether
+ a category of alarms will be visited or not. *)
type flags = {
remove_trivial: bool;
initialized: bool;
@@ -42,7 +72,7 @@ type flags = {
bool_value: bool;
}
-(** Defaults are taken from the Kernel and RTE plug-in options *)
+(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
val default :
?remove_trivial:bool ->
?initialized:bool ->
@@ -61,21 +91,34 @@ val default :
?bool_value:bool ->
unit -> flags
-(** All flags set to [true] *)
+(** All flags set to [true]. *)
val flags_all : flags
-(** All flags set to [false] *)
+(** All flags set to [false]. *)
val flags_none : flags
-(** Low-level iterators callback.
+(** {2 Low-Level RTE Iterators}
+
+ RTE Iterators allow to traverse a Cil AST fragment (stmt, expr, l-value)
+ and reveal its potential Alarms. Each alarm will be presented to a callback
+ with type [on_alarm], that you can use in turn to generate an annotation
+ or perform any other treatment.
+
+ Flags can be used to select which alarm categories to visit, with
+ defaults derived from Kernel and RTE plug-in parameters.
+*)
+
+(** Alarm callback.
+
+ The [on_alarm kf stmt ~invalid alarm] callback is invoked on each
+ alarm visited by an RTE iterator, provided it fits the selected categories.
+ The [kf] and [stmt] designates the statement originating the alarm,
+ while [~invalid:true] is set when the alarm trivially evaluates to false.
+ In this later case, the corresponding annotation shall be assigned
+ the status [False_if_reachable].
- The [on_alarm stmt ?status alarm] callback is invoked with
- the [stmt] originating the alarm and the already known status,
- if any.
*)
-type on_alarm =
- kinstr -> ?status:Property_status.emitted_status ->
- Alarms.alarm -> unit
+type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
(** Low-level iterators
@@ -89,35 +132,27 @@ type on_alarm =
type 'a iterator =
?flags:flags -> on_alarm ->
- Kernel_function.t ->
- Cil_types.stmt ->
- 'a -> unit
+ Kernel_function.t -> Cil_types.stmt -> 'a -> unit
val iter_lval : lval iterator
val iter_exp : exp iterator
val iter_instr : instr iterator
val iter_stmt : stmt iterator
-(** Generates RTE for a single function. Uses the status of the various
- RTE options do decide which kinds of annotations must be generated.
-*)
-val annotate_kf: kernel_function -> unit
-
-(** Generates all RTEs for a given function. *)
-val do_all_rte: kernel_function -> unit
+(** {2 Alarm Helpers} *)
-(** Generates all RTEs except preconditions for a given function. *)
-val do_rte: kernel_function -> unit
+(** Returns a [False_if_reachable] status when invalid. *)
+val status : invalid:bool -> Property_status.emitted_status option
-val rte_annotations: stmt -> code_annotation list
-val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
-val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
+(** Registers and returns the annotation associated with the alarm,
+ and a boolean flag indicating whether it has been freshly generated
+ or not. *)
+val annotation :
+ Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
+ code_annotation * bool
-(** Main entry point of the plug-in, used by [-rte] option: computes
- RTE on the whole AST. Which kind of RTE is generated depends on the
- options given on the command line.
-*)
-val compute: unit -> unit
+(** A callback that simply register the annotation associated with the alarm. *)
+val register : Emitter.t -> on_alarm
(*
Local Variables: