diff --git a/Makefile b/Makefile
index 1668a9d2777578fe6d3149774945eaedd101e369..be71d63e14ec90e788cbbf3991707faf9aa956a4 100644
--- a/Makefile
+++ b/Makefile
@@ -957,7 +957,7 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
PLUGIN_ENABLE:=$(ENABLE_RTEGEN)
PLUGIN_NAME:=RteGen
PLUGIN_DIR:=src/plugins/rte
-PLUGIN_CMO:= options generator rte visit register
+PLUGIN_CMO:= options generator rte flags visit register
PLUGIN_DISTRIBUTED:=yes
PLUGIN_INTERNAL_TEST:=yes
PLUGIN_TESTS_DIRS:=rte rte_manual
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index dd34d6c7e782c8eb929528844e2b9d94027eb2d7..37041b02d29df294ff1fa3b9326be5b9dd58aaec 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1002,6 +1002,8 @@ src/plugins/report/report_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/scan.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/scan.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/RteGen.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/rte/flags.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/rte/flags.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/generator.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/generator.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/options.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index 0357b823a5518c66459726fa4e5fa944f556a83d..37f64d20dc038c9a4f3c1212ffeb8cfc338a1289 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -20,7 +20,32 @@
(* *)
(**************************************************************************)
-(** Some functions are also registered in {!Db.Value}. *)
+(** Consult internal plug-in documentation for more details *)
+
+(** Flags for filtering Alarms *)
+module Flags : module type of Flags
+
+(** RTE Generator Status & Emitters *)
+module Generator : module type of Generator
(** Visitors to iterate over Alarms and/or generate Code-Annotations *)
-module Visit : module type of Visit
+module Visit : sig
+ open Cil_types
+ val annotate_kf: kernel_function -> unit
+ val do_all_rte: kernel_function -> unit
+ val do_rte: kernel_function -> unit
+ val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
+ val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
+ val compute: unit -> unit
+ type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
+ type 'a iterator = ?flags:Flags.t -> on_alarm ->
+ 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
+ val annotation :
+ Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
+ code_annotation * bool
+ val register : Emitter.t -> on_alarm
+end
diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
new file mode 100644
index 0000000000000000000000000000000000000000..eed7aa13716ac2e69ce7b4999c1402f04ef5ece8
--- /dev/null
+++ b/src/plugins/rte/flags.ml
@@ -0,0 +1,121 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Fine Tuning Visitors --- *)
+(* -------------------------------------------------------------------------- *)
+
+type t = {
+ remove_trivial: bool;
+ initialized: bool;
+ mem_access: bool;
+ div_mod: bool;
+ shift: bool;
+ left_shift_negative: bool;
+ right_shift_negative: bool;
+ signed_overflow: bool;
+ unsigned_overflow: bool;
+ signed_downcast: bool;
+ unsigned_downcast: bool;
+ float_to_int: bool;
+ finite_float: bool;
+ pointer_call: bool;
+ bool_value: bool;
+}
+
+let all = {
+ remove_trivial = true;
+ initialized = true;
+ mem_access = true;
+ div_mod = true;
+ shift = true;
+ left_shift_negative = true;
+ right_shift_negative = true;
+ signed_overflow = true;
+ unsigned_overflow = true;
+ signed_downcast = true;
+ unsigned_downcast = true;
+ float_to_int = true;
+ finite_float = true;
+ pointer_call = true;
+ bool_value = true;
+}
+
+let none = {
+ remove_trivial = false;
+ initialized = false;
+ mem_access = false;
+ div_mod = false;
+ shift = false;
+ left_shift_negative = false;
+ right_shift_negative = false;
+ signed_overflow = false;
+ unsigned_overflow = false;
+ signed_downcast = false;
+ unsigned_downcast = false;
+ float_to_int = false;
+ finite_float = false;
+ pointer_call = false;
+ bool_value = false;
+}
+
+(* Which annotations should be added,
+ from local options, or deduced from the options of RTE and the kernel *)
+
+let option (get : unit -> bool) = function None -> get () | Some flag -> flag
+
+let default
+ ?remove_trivial
+ ?initialized
+ ?mem_access
+ ?div_mod
+ ?shift
+ ?left_shift_negative
+ ?right_shift_negative
+ ?signed_overflow
+ ?unsigned_overflow
+ ?signed_downcast
+ ?unsigned_downcast
+ ?float_to_int
+ ?finite_float
+ ?pointer_call
+ ?bool_value
+ () =
+ {
+ remove_trivial = option (fun () -> not (Options.Trivial.get ())) remove_trivial ;
+ initialized = option Options.DoInitialized.get initialized ;
+ mem_access = option Options.DoMemAccess.get mem_access ;
+ div_mod = option Options.DoDivMod.get div_mod ;
+ shift = option Options.DoShift.get shift;
+ left_shift_negative = option Kernel.LeftShiftNegative.get left_shift_negative ;
+ right_shift_negative = option Kernel.RightShiftNegative.get right_shift_negative ;
+ signed_overflow = option Kernel.SignedOverflow.get signed_overflow ;
+ unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
+ signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
+ unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
+ float_to_int = option Options.DoFloatToInt.get float_to_int ;
+ finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
+ pointer_call = option Options.DoPointerCall.get pointer_call ;
+ bool_value = option Kernel.InvalidBool.get bool_value ;
+ }
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli
new file mode 100644
index 0000000000000000000000000000000000000000..578ba9ef3088b857eb9fed011be515f5096f90d4
--- /dev/null
+++ b/src/plugins/rte/flags.mli
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Filtering Categories of Alarms *)
+(* -------------------------------------------------------------------------- *)
+
+(** Flags for controling the low-level API. Each flag control whether
+ a category of alarms will be visited or not. *)
+type t = {
+ remove_trivial: bool;
+ initialized: bool;
+ mem_access: bool;
+ div_mod: bool;
+ shift: bool;
+ left_shift_negative: bool;
+ right_shift_negative: bool;
+ signed_overflow: bool;
+ unsigned_overflow: bool;
+ signed_downcast: bool;
+ unsigned_downcast: bool;
+ float_to_int: bool;
+ finite_float: bool;
+ pointer_call: bool;
+ bool_value: bool;
+}
+
+(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
+val default :
+ ?remove_trivial:bool ->
+ ?initialized:bool ->
+ ?mem_access:bool ->
+ ?div_mod:bool ->
+ ?shift:bool ->
+ ?left_shift_negative:bool ->
+ ?right_shift_negative:bool ->
+ ?signed_overflow:bool ->
+ ?unsigned_overflow:bool ->
+ ?signed_downcast:bool ->
+ ?unsigned_downcast:bool ->
+ ?float_to_int:bool ->
+ ?finite_float:bool ->
+ ?pointer_call:bool ->
+ ?bool_value:bool ->
+ unit -> t
+
+(** All flags set to [true]. *)
+val all : t
+
+(** All flags set to [false]. *)
+val none : t
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index a47464475015f9df6a626f49e7e30309103b6bd8..4487c5bdfff69e63cfb4081ae3a4d30e307535e7 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -24,128 +24,10 @@
open Cil_types
open Cil_datatype
+open Flags
(* AST inplace visitor for runtime annotation generation *)
-(* module for bypassing categories of annotation generation for certain
- expression ids ;
- useful in a case such as
-
- signed char cx,cy,cz;
- cz = cx * cy;
-
- which translates to
-
- cz = (signed char) ((int) cx * (int) cz) ;
-
- which would in this case be annotated both by
-
- assert
- (((int )cx+(int )cy <= 2147483647) and
- ((int )cx+(int )cy >= (-0x7FFFFFFF-1)));
-
- and
-
- assert (((int )cx+(int )cy <= 127) and ((int )cx+(int )cy >= -128));
-
- while we only want to keep the second assert (comes from the cast,
- and is stronger)
-*)
-
-type flags = {
- remove_trivial: bool;
- initialized: bool;
- mem_access: bool;
- div_mod: bool;
- shift: bool;
- left_shift_negative: bool;
- right_shift_negative: bool;
- signed_overflow: bool;
- unsigned_overflow: bool;
- signed_downcast: bool;
- unsigned_downcast: bool;
- float_to_int: bool;
- finite_float: bool;
- pointer_call: bool;
- bool_value: bool;
-}
-
-let flags_all = {
- remove_trivial = true;
- initialized = true;
- mem_access = true;
- div_mod = true;
- shift = true;
- left_shift_negative = true;
- right_shift_negative = true;
- signed_overflow = true;
- unsigned_overflow = true;
- signed_downcast = true;
- unsigned_downcast = true;
- float_to_int = true;
- finite_float = true;
- pointer_call = true;
- bool_value = true;
-}
-
-let flags_none = {
- remove_trivial = false;
- initialized = false;
- mem_access = false;
- div_mod = false;
- shift = false;
- left_shift_negative = false;
- right_shift_negative = false;
- signed_overflow = false;
- unsigned_overflow = false;
- signed_downcast = false;
- unsigned_downcast = false;
- float_to_int = false;
- finite_float = false;
- pointer_call = false;
- bool_value = false;
-}
-
-(* Which annotations should be added,
- from local options, or deduced from the options of RTE and the kernel *)
-
-let option (get : unit -> bool) = function None -> get () | Some flag -> flag
-
-let default
- ?remove_trivial
- ?initialized
- ?mem_access
- ?div_mod
- ?shift
- ?left_shift_negative
- ?right_shift_negative
- ?signed_overflow
- ?unsigned_overflow
- ?signed_downcast
- ?unsigned_downcast
- ?float_to_int
- ?finite_float
- ?pointer_call
- ?bool_value
- () =
- {
- remove_trivial = option (fun () -> not (Options.Trivial.get ())) remove_trivial ;
- initialized = option Options.DoInitialized.get initialized ;
- mem_access = option Options.DoMemAccess.get mem_access ;
- div_mod = option Options.DoDivMod.get div_mod ;
- shift = option Options.DoShift.get shift;
- left_shift_negative = option Kernel.LeftShiftNegative.get left_shift_negative ;
- right_shift_negative = option Kernel.RightShiftNegative.get right_shift_negative ;
- signed_overflow = option Kernel.SignedOverflow.get signed_overflow ;
- unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
- signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
- unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
- float_to_int = option Options.DoFloatToInt.get float_to_int ;
- finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
- pointer_call = option Options.DoPointerCall.get pointer_call ;
- bool_value = option Kernel.InvalidBool.get bool_value ;
- }
-
(** [kf]: function to annotate
[flags]: which RTE to generate.
[register]: the action to perform on each RTE alarm *)
@@ -472,7 +354,7 @@ let iter_alarms visit ?flags (on_alarm:on_alarm) kf stmt element =
ignore (visit (visitor :> Cil.cilVisitor) element)
type 'a iterator =
- ?flags:flags -> on_alarm ->
+ ?flags:Flags.t -> on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
let iter_lval : lval iterator = iter_alarms Cil.visitCilLval
@@ -573,7 +455,7 @@ let annotate_kf kf = annotate_kf_aux (default ()) kf
function *)
let do_all_rte kf =
let flags =
- { flags_all with
+ { Flags.all with
signed_downcast = false;
unsigned_downcast = false; }
in
@@ -583,7 +465,7 @@ let do_all_rte kf =
function *)
let do_rte kf =
let flags =
- { flags_all with
+ { Flags.all with
unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false; }
diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli
index 1127c3c52b9a64d217b44f32edef1c817a21ce60..9c909a5706c6dc63a184f4b732a91c0f812c5650 100644
--- a/src/plugins/rte/visit.mli
+++ b/src/plugins/rte/visit.mli
@@ -49,53 +49,6 @@ val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
*)
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;
- mem_access: bool;
- div_mod: bool;
- shift: bool;
- left_shift_negative: bool;
- right_shift_negative: bool;
- signed_overflow: bool;
- unsigned_overflow: bool;
- signed_downcast: bool;
- unsigned_downcast: bool;
- float_to_int: bool;
- finite_float: bool;
- pointer_call: bool;
- bool_value: bool;
-}
-
-(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
-val default :
- ?remove_trivial:bool ->
- ?initialized:bool ->
- ?mem_access:bool ->
- ?div_mod:bool ->
- ?shift:bool ->
- ?left_shift_negative:bool ->
- ?right_shift_negative:bool ->
- ?signed_overflow:bool ->
- ?unsigned_overflow:bool ->
- ?signed_downcast:bool ->
- ?unsigned_downcast:bool ->
- ?float_to_int:bool ->
- ?finite_float:bool ->
- ?pointer_call:bool ->
- ?bool_value:bool ->
- unit -> flags
-
-(** All flags set to [true]. *)
-val flags_all : flags
-
-(** All flags set to [false]. *)
-val flags_none : flags
-
(** {2 Low-Level RTE Iterators}
RTE Iterators allow to traverse a Cil AST fragment (stmt, expr, l-value)
@@ -120,8 +73,7 @@ val flags_none : flags
type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
(** Type of low-level iterators visiting an element ['a] of the AST *)
-type 'a iterator =
- ?flags:flags -> on_alarm ->
+type 'a iterator = ?flags:Flags.t -> on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
val iter_lval : lval iterator