diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index a35cbf068533b07824f911b6b715480f7570e117..539411cd3e6f333e884bc9c2f1702c8fdb6d32a1 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -839,30 +839,6 @@ module Security = struct
let self = ref State.dummy
end
-module RteGen = struct
- type status_accessor =
- string * (kernel_function -> bool -> unit) * (kernel_function -> bool)
- let compute = mk_fun "RteGen.compute"
- let annotate_kf = mk_fun "RteGen.annotate_kf"
- let self = ref State.dummy
- let do_all_rte = mk_fun "RteGen.do_all_rte"
- let do_rte = mk_fun "RteGen.do_rte"
- let get_all_status = mk_fun "RteGen.get_all_status"
- let get_signedOv_status = mk_fun "RteGen.get_signedOv_status"
- let get_divMod_status = mk_fun "RteGen.get_divMod_status"
- let get_initialized_status = mk_fun "RteGen.get_initialized_status"
- let get_signed_downCast_status = mk_fun "RteGen.get_signed_downCast_status"
- let get_memAccess_status = mk_fun "RteGen.get_memAccess_status"
- let get_pointerCall_status = mk_fun "RteGen.get_pointerCall_status"
- let get_unsignedOv_status = mk_fun "RteGen.get_unsignedOv_status"
- let get_unsignedDownCast_status = mk_fun "RteGen.get_unsignedDownCast_status"
- let get_pointer_downcast_status = mk_fun "RteGen.get_pointer_downcast_status"
- let get_float_to_int_status = mk_fun "RteGen.get_float_to_int_status"
- let get_finite_float_status = mk_fun "RteGen.get_finite_float_status"
- let get_pointer_value_status = mk_fun "RteGen.get_pointer_value_status"
- let get_bool_value_status = mk_fun "RteGen.get_bool_value_status"
-end
-
module PostdominatorsTypes = struct
exception Top
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 7b072132ade4ebb828bd4e1e81d72b8a45c9af5f..cdf6565253e401472131c324436f6b7de1dd7645 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -754,48 +754,6 @@ module Postdominators: PostdominatorsTypes.Sig
@see <../postdominators/index.html> internal documentation. *)
module PostdominatorsValue: PostdominatorsTypes.Sig
-(** Runtime Error Annotation Generation plugin.
- @see <../rte/index.html> internal documentation. *)
-module RteGen : sig
- (** Same result as having [-rte] on the command line*)
- val compute : (unit -> unit) ref
-
- (** 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) ref
-
- (** Generates all possible RTE for a given function. *)
- val do_all_rte : (kernel_function -> unit) ref
-
- (** Generates all possible RTE except pre-conditions for a given function. *)
- val do_rte : (kernel_function -> unit) ref
-
- val self: State.t ref
- type status_accessor =
- string (* name *)
- * (kernel_function -> bool -> unit) (* for each kf and each kind of
- annotation, set/unset the fact
- that there has been generated *)
- * (kernel_function -> bool) (* is this kind of annotation generated in
- kf? *)
- val get_all_status : (unit -> status_accessor list) ref
- val get_divMod_status : (unit -> status_accessor) ref
- val get_initialized_status: (unit -> status_accessor) ref
- val get_memAccess_status : (unit -> status_accessor) ref
- val get_pointerCall_status: (unit -> status_accessor) ref
- val get_signedOv_status : (unit -> status_accessor) ref
- val get_signed_downCast_status : (unit -> status_accessor) ref
- val get_unsignedOv_status : (unit -> status_accessor) ref
- val get_unsignedDownCast_status : (unit -> status_accessor) ref
- val get_pointer_downcast_status : (unit -> status_accessor) ref
- val get_float_to_int_status : (unit -> status_accessor) ref
- val get_finite_float_status : (unit -> status_accessor) ref
- val get_pointer_value_status : (unit -> status_accessor) ref
- val get_bool_value_status : (unit -> status_accessor) ref
-end
-
-
(** Security analysis.
@see <../security/index.html> internal documentation. *)
module Security : sig
diff --git a/src/plugins/e-acsl/src/analyses/rte.ml b/src/plugins/e-acsl/src/analyses/rte.ml
index f542d1fee0f3b61efdb847350a3b0cbed9d89db5..a800c4367011121d37784d085848e9c406f0927c 100644
--- a/src/plugins/e-acsl/src/analyses/rte.ml
+++ b/src/plugins/e-acsl/src/analyses/rte.ml
@@ -20,45 +20,18 @@
(* *)
(**************************************************************************)
-(* ************************************************************************** *)
-(** {2 Generic code} *)
-(* ************************************************************************** *)
-
-let warn_rte warn exn =
- if warn then
- Options.warning "@[@[cannot run RTE:@ %s.@]@ \
- Ignoring potential runtime errors in annotations."
- (Printexc.to_string exn)
-
(* ************************************************************************** *)
(** {2 Exported code} *)
(* ************************************************************************** *)
-open Cil_datatype
+let stmt ?warn:_ kf stmt =
+ RteGen.Visit.get_annotations_stmt kf stmt
-let stmt ?(warn=true) =
- try
- Dynamic.get
- ~plugin:"RteGen"
- "stmt_annotations"
- (Datatype.func2 Kernel_function.ty Stmt.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
- with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
- ->
- warn_rte warn exn;
- fun _ _ -> []
+let exp ?warn:_ kf stmt e =
+ RteGen.Visit.get_annotations_exp kf stmt e
-let exp ?(warn=true) =
- try
- Dynamic.get
- ~plugin:"RteGen"
- "exp_annotations"
- (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
- with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
- ->
- warn_rte warn exn;
- fun _ _ _ -> []
+let get_state_selection_with_dependencies () =
+ State_selection.with_dependencies RteGen.Api.self
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/analyses/rte.mli b/src/plugins/e-acsl/src/analyses/rte.mli
index f4697989d10357fe1a6b3f994e835612c549e232..9327156800923f7a5792b091202a7f3caf74bac7 100644
--- a/src/plugins/e-acsl/src/analyses/rte.mli
+++ b/src/plugins/e-acsl/src/analyses/rte.mli
@@ -30,6 +30,10 @@ val stmt: ?warn:bool -> kernel_function -> stmt -> code_annotation list
val exp: ?warn:bool -> kernel_function -> stmt -> exp -> code_annotation list
(** RTEs of a given exp, as a list of code annotations. *)
+val get_state_selection_with_dependencies: unit -> State_selection.t
+(** Equivalent to [State_selection.with_dependencies RteGen.Api.self]
+ if the RTE plug-in is enabled, empty otherwise. *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/dune b/src/plugins/e-acsl/src/dune
index bd9049b7cd9366699ccfdc3478c66815907decd2..f52b8949ea2346ce9b8a26c80a09341acbcf1c08 100644
--- a/src/plugins/e-acsl/src/dune
+++ b/src/plugins/e-acsl/src/dune
@@ -25,6 +25,7 @@
(deps (universe))
(action (progn
(echo "E-ACSL:" %{lib-available:frama-c-e-acsl.core} "\n")
+ (echo " - Rtegen:" %{lib-available:frama-c-rtegen.core} "\n")
)
)
)
@@ -34,7 +35,7 @@
(optional)
(public_name frama-c-e-acsl.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel))
+ (libraries frama-c.kernel frama-c-rtegen.core))
(plugin (optional) (name e-acsl) (libraries frama-c-e-acsl.core) (site (frama-c plugins)))
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index e7eba10fee47a673173279c634d3003b044b47c1..54342436cdfce2c5e844da13e3ad604e4045b8a1 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -77,7 +77,7 @@ let generate_code =
redoing the RTE management system *)
let selection =
State_selection.union
- (State_selection.with_dependencies !Db.RteGen.self)
+ (Rte.get_state_selection_with_dependencies ())
(State_selection.with_dependencies Options.Run.self)
in
Project.clear ~selection ~project:copied_prj ();
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index 5e18605413afa48366ddb8326f9c8d32d36cc87d..772c1e44bfaf425f6a2bd71c3753352091b1901d 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -277,8 +277,6 @@ sig
end
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/dune b/src/plugins/gui/dune
index b236414fc979c75878b1813a68996983bb6e7828..6bd7f4534326ed74b26ced2f6f503272d1a04a30 100644
--- a/src/plugins/gui/dune
+++ b/src/plugins/gui/dune
@@ -30,6 +30,8 @@
(echo " - lablgtk2.sourceview2:" %{lib-available:lablgtk2.sourceview2} "\n")
(echo " - lablgtk3:" %{lib-available:lablgtk3} "\n")
(echo " - lablgtk3-sourceview3:" %{lib-available:lablgtk3-sourceview3} "\n")
+ ; From a GUI hook registered by RteGen.
+ (echo " - Rtegen (optional):" %{lib-available:frama-c-rtegen.core} "\n")
)
)
)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 0566095701dc9db9eb6c119ed6c131df250cf440..b74002a0008dadf81b51835c1cd0156c86831e05 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -20,6 +20,15 @@
(* *)
(**************************************************************************)
+module Rte = struct
+ type status_accessor =
+ string
+ * (Cil_types.kernel_function -> bool -> unit)
+ * (Cil_types.kernel_function -> bool)
+ let get_all_status: (unit -> status_accessor list) option ref = ref None
+ let register_get_all_status getter = get_all_status := Some getter
+end
+
open Design
open Cil_types
open Property_status
@@ -220,6 +229,10 @@ struct
checks := chk :: !checks;
chk
+ let hint_rte hint =
+ if Option.is_some !Rte.get_all_status then hint
+ else hint ^ " (but RteGen plugin is inactive)"
+
let onlyCurrent = add ~name:"Current function" ~default:false
~hint:"Only show properties related to current function" ()
@@ -248,7 +261,7 @@ struct
(* Function called when RTEs are enabled or disabled. *)
let set_rte = ref (fun _b -> ())
let rte = add ~set:(fun b -> !set_rte b) ~name:"RTEs"
- ~hint:"Show runtime errors" ()
+ ~hint:(hint_rte "Show runtime errors") ()
let invariant = add ~name:"Invariant"
~hint:"Show loop invariants" ()
let variant = add ~name:"Variant"
@@ -273,9 +286,9 @@ struct
~hint:"Show 'reachable' hypotheses" ()
let rteNotGenerated = add ~default:false ~name:"Non generated"
- ~hint:"Show RTEs assertions that remain to generate" ()
+ ~hint:(hint_rte "Show RTEs assertions that remain to generate") ()
let rteGenerated = add ~default:false ~name:"Generated"
- ~hint:"Show RTEs assertions that have been generated" ()
+ ~hint:(hint_rte "Show RTEs assertions that have been generated") ()
let valid = add ~name:"Valid"
~hint:"Show properties that are proven valid" ()
@@ -408,7 +421,7 @@ open Refreshers
(* Process the rte statuses for the given kf, and add the result in the
accumulator. Filter the statuses according to user-selected filters*)
-let aux_rte kf acc (name, _, rte_status_get: Db.RteGen.status_accessor) =
+let aux_rte kf acc (name, _, rte_status_get: Rte.status_accessor) =
let st = rte_status_get kf in
match st, rteGenerated.get (), rteNotGenerated.get () with
| true, true, _
@@ -705,7 +718,10 @@ let make_panel (main_ui:main_window_extension_points) =
) main_ui#file_tree#selected_globals)
in
- let rte_get_all_statuses = !Db.RteGen.get_all_status () in
+ let rte_get_all_statuses = match !Rte.get_all_status with
+ | None -> []
+ | Some registered_getter -> registered_getter ()
+ in
(* All non-filtered RTE statuses for a given function *)
let rte_kf kf = List.fold_left (aux_rte kf) [] rte_get_all_statuses in
(* Add RTE statuses for all functions. We cannot simply iterate over
diff --git a/src/plugins/gui/property_navigator.mli b/src/plugins/gui/property_navigator.mli
index 4837d8d7d0f79516db07514c5fceda0e31151cd4..385268930e51e8e084ad8af20345badb2fe9dd85 100644
--- a/src/plugins/gui/property_navigator.mli
+++ b/src/plugins/gui/property_navigator.mli
@@ -20,10 +20,15 @@
(* *)
(**************************************************************************)
-(** Extension of the GUI in order to navigate in ACSL properties.
- No function is exported. *)
+(** Extension of the GUI in order to navigate in ACSL properties. *)
-(* Empty on purpose. *)
+module Rte: sig
+ type status_accessor =
+ string
+ * (Cil_types.kernel_function -> bool -> unit)
+ * (Cil_types.kernel_function -> bool)
+ val register_get_all_status : (unit -> status_accessor list) -> unit
+end
(*
Local Variables:
diff --git a/src/plugins/rte/RteGen.ml b/src/plugins/rte/RteGen.ml
index 938489dcdd015a6b646fc62f9cd9d9ccd19e7448..c6e78945374e534d94e7f94fdc7314416ecfa00a 100644
--- a/src/plugins/rte/RteGen.ml
+++ b/src/plugins/rte/RteGen.ml
@@ -28,3 +28,6 @@ module Generator = Generator
(** Visitors to iterate over Alarms and/or generate Code-Annotations *)
module Visit = Visit
+
+(** Replaces old Db API *)
+module Api = Api
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index 5b0438dd6933108ac53fe34c7301f90005774232..39219e1965dbd233cc354fb39081d940f4555e53 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -57,3 +57,6 @@ module Visit : sig
Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
code_annotation * bool
end
+
+(** Replaces old Db API *)
+module Api : module type of Api
diff --git a/src/plugins/rte/api.ml b/src/plugins/rte/api.ml
new file mode 100644
index 0000000000000000000000000000000000000000..02b9dda954a52a8db55b05b857894f403e27364a
--- /dev/null
+++ b/src/plugins/rte/api.ml
@@ -0,0 +1,87 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* state *)
+(* -------------------------------------------------------------------------- *)
+
+let self = Generator.self
+
+(* -------------------------------------------------------------------------- *)
+(* getters *)
+(* -------------------------------------------------------------------------- *)
+
+type status_accessor = Generator.status_accessor
+
+let get_all_status () = Generator.all_statuses
+let get_signedOv_status () = Generator.Signed_overflow.accessor
+let get_divMod_status () = Generator.Div_mod.accessor
+let get_initialized_status () = Generator.Initialized.accessor
+let get_signed_downCast_status () = Generator.Signed_downcast.accessor
+let get_memAccess_status () = Generator.Mem_access.accessor
+let get_pointerCall_status () = Generator.Pointer_call.accessor
+let get_unsignedOv_status () = Generator.Unsigned_overflow.accessor
+let get_unsignedDownCast_status () = Generator.Unsigned_downcast.accessor
+let get_pointer_downcast_status () = Generator. Pointer_downcast.accessor
+let get_float_to_int_status () = Generator.Float_to_int.accessor
+let get_finite_float_status () = Generator.Finite_float.accessor
+let get_pointer_value_status () = Generator.Pointer_value.accessor
+let get_bool_value_status () = Generator.Bool_value.accessor
+
+
+(* -------------------------------------------------------------------------- *)
+(* dedicated computations *)
+(* -------------------------------------------------------------------------- *)
+
+let annotate_kf kf = Visit.annotate kf
+
+(* annotate for all rte + unsigned overflows (which are not rte), for a given
+ function *)
+let do_all_rte kf =
+ let flags =
+ { (Flags.all ()) with
+ Flags.signed_downcast = false;
+ unsigned_downcast = false; }
+ in
+ Visit.annotate ~flags kf
+
+(* annotate for rte only (not unsigned overflows and downcasts) for a given
+ function *)
+let do_rte kf =
+ let flags =
+ { (Flags.all ()) with
+ Flags.unsigned_overflow = false;
+ signed_downcast = false;
+ unsigned_downcast = false; }
+ in
+ Visit.annotate ~flags kf
+
+let compute () =
+ (* compute RTE annotations, whether Enabled is set or not *)
+ Ast.compute () ;
+ let include_function kf =
+ let fsel = Options.FunctionSelection.get () in
+ Kernel_function.Set.is_empty fsel
+ || Kernel_function.Set.mem kf fsel
+ in
+ Globals.Functions.iter
+ (fun kf -> if include_function kf then annotate_kf kf)
diff --git a/src/plugins/rte/api.mli b/src/plugins/rte/api.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b30ef13b48cd7eb277c0139c927eb853083058c2
--- /dev/null
+++ b/src/plugins/rte/api.mli
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Runtime Error Annotation Generation plugin.
+ @see <./index.html> internal documentation. *)
+
+(** Same result as having [-rte] on the command line*)
+val compute : unit -> unit
+
+(** 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 : Cil_types.kernel_function -> unit
+
+(** Generates all possible RTE for a given function. *)
+val do_all_rte : Cil_types.kernel_function -> unit
+
+(** Generates all possible RTE except pre-conditions for a given function. *)
+val do_rte : Cil_types.kernel_function -> unit
+
+val self: State.t
+
+type status_accessor =
+ string (* name *)
+ * (Cil_types.kernel_function -> bool -> unit) (* for each kf and each kind of
+ annotation, set/unset the
+ fact that there has been
+ generated *)
+ * (Cil_types.kernel_function -> bool) (* is this kind of annotation generated
+ in kf? *)
+
+val get_all_status : unit -> status_accessor list
+val get_divMod_status : unit -> status_accessor
+val get_initialized_status: unit -> status_accessor
+val get_memAccess_status : unit -> status_accessor
+val get_pointerCall_status: unit -> status_accessor
+val get_signedOv_status : unit -> status_accessor
+val get_signed_downCast_status : unit -> status_accessor
+val get_unsignedOv_status : unit -> status_accessor
+val get_unsignedDownCast_status : unit -> status_accessor
+val get_pointer_downcast_status : unit -> status_accessor
+val get_float_to_int_status : unit -> status_accessor
+val get_finite_float_status : unit -> status_accessor
+val get_pointer_value_status : unit -> status_accessor
+val get_bool_value_status : unit -> status_accessor
diff --git a/src/plugins/rte/dune b/src/plugins/rte/dune
index cadaf87df3807fd54fc34235fdc696a5a4f801f3..6ef36116c611e5ebfc7eac0a484e65cbe50470f4 100644
--- a/src/plugins/rte/dune
+++ b/src/plugins/rte/dune
@@ -33,7 +33,7 @@
(name RteGen)
(optional)
(public_name frama-c-rtegen.core)
- (private_modules options generator rte visit register)
+ (private_modules api options generator rte visit register)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
)
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index ecb7b7255ffdb0310b1fa2a66ad079b0bf87b621..5f1f345d5f3a4733df5ecde28e1d7d5a5671d074 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -22,14 +22,19 @@
open Cil_types
+type status_accessor =
+ string
+ * (Cil_types.kernel_function -> bool -> unit)
+ * (Cil_types.kernel_function -> bool)
+
module type S = sig
val is_computed: kernel_function -> bool
val set: kernel_function -> bool -> unit
- val accessor: Db.RteGen.status_accessor
+ val accessor: status_accessor
end
let states : State.t list ref = ref []
-let accessors : Db.RteGen.status_accessor list ref = ref []
+let accessors : status_accessor list ref = ref []
module Make
(M:sig
@@ -202,7 +207,6 @@ let proxy =
State_builder.Proxy.create "RTE" State_builder.Proxy.Backward !states
let self = State_builder.Proxy.get proxy
-let () = Db.RteGen.self := self
let all_statuses = !accessors
diff --git a/src/plugins/rte/generator.mli b/src/plugins/rte/generator.mli
index 6f3a90ec4650f7e04c86dfa055e0259f953cd558..e8ea06569156a63e581fc558023b7b0350663de8 100644
--- a/src/plugins/rte/generator.mli
+++ b/src/plugins/rte/generator.mli
@@ -20,10 +20,18 @@
(* *)
(**************************************************************************)
+type status_accessor =
+ string (* name *)
+ * (Cil_types.kernel_function -> bool -> unit) (* for each kf and each kind of
+ annotation, set/unset the
+ fact that there has been
+ generated *)
+ * (Cil_types.kernel_function -> bool) (* is this kind of annotation generated
+ in kf? *)
module type S = sig
val is_computed: Kernel_function.t -> bool
val set: Kernel_function.t -> bool -> unit
- val accessor: Db.RteGen.status_accessor
+ val accessor: status_accessor
end
(* No module for Trivial: dependency added for generators below *)
@@ -45,7 +53,7 @@ module Float_to_int: S
module Finite_float: S
module Bool_value: S
-val all_statuses: Db.RteGen.status_accessor list
+val all_statuses: status_accessor list
(** The Emitter for Annotations registered by RTE *)
val emitter: Emitter.t
@@ -55,6 +63,8 @@ open Cil_types
(** Returns all annotations actually {i registered} by RTE so far *)
val get_registered_annotations: stmt -> code_annotation list
+val self: State.t
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/rte/gui/dune b/src/plugins/rte/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..40fb178bcfcebd877a5f7f72755167b27e998f72
--- /dev/null
+++ b/src/plugins/rte/gui/dune
@@ -0,0 +1,43 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Rtegen GUI:" %{lib-available:frama-c-studia.gui} "\n")
+ (echo " - Frama-C GUI:" %{lib-available:frama-c.gui} "\n")
+ (echo " - Rtegen:" %{lib-available:frama-c-rtegen.core} "\n")
+
+ )
+ )
+)
+
+( library
+ (name rtegen_gui)
+ (public_name frama-c-rtegen.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open RteGen :standard -w -9)
+ (libraries frama-c.kernel frama-c.gui frama-c-rtegen.core)
+)
+
+(plugin (optional) (name rtegen-gui) (libraries frama-c-rtegen.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/rte/gui/rtegen_gui.ml b/src/plugins/rte/gui/rtegen_gui.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3e458cf3e910cf1a68a99cb528e7ac9f17e00db2
--- /dev/null
+++ b/src/plugins/rte/gui/rtegen_gui.ml
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let () =
+ Property_navigator.Rte.register_get_all_status RteGen.Api.get_all_status
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 12af98e3b6dcb4ed74098961dd63be4c80a2e86b..9f549023e906b80b73c9c9ed0a3e91dcba949b56 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -20,81 +20,15 @@
(* *)
(**************************************************************************)
-(* -------------------------------------------------------------------------- *)
-(* dedicated computations *)
-(* -------------------------------------------------------------------------- *)
-
-(* annotate for all rte + unsigned overflows (which are not rte), for a given
- function *)
-let do_all_rte kf =
- let flags =
- { (Flags.all ()) with
- Flags.signed_downcast = false;
- unsigned_downcast = false; }
- in
- Visit.annotate ~flags kf
-
-(* annotate for rte only (not unsigned overflows and downcasts) for a given
- function *)
-let do_rte kf =
- let flags =
- { (Flags.all ()) with
- Flags.unsigned_overflow = false;
- signed_downcast = false;
- unsigned_downcast = false; }
- in
- Visit.annotate ~flags kf
-
-let compute () =
- (* compute RTE annotations, whether Enabled is set or not *)
- Ast.compute () ;
- let include_function kf =
- let fsel = Options.FunctionSelection.get () in
- Kernel_function.Set.is_empty fsel
- || Kernel_function.Set.mem kf fsel
- in
- Globals.Functions.iter
- (fun kf -> if include_function kf then !Db.RteGen.annotate_kf kf)
-
-let () =
- Db.register Db.RteGen.annotate_kf Visit.annotate;
- Db.register Db.RteGen.compute compute;
- Db.register Db.RteGen.do_rte do_rte;
-
- Db.register Db.RteGen.do_all_rte do_all_rte;
- let _ignore =
- Dynamic.register
- ~comment:"Generate all RTE annotations in the given function."
- ~plugin:"RteGen"
- "do_all_rte"
- (Datatype.func Kernel_function.ty Datatype.unit)
- do_all_rte
- in
-
- let open Generator in
- let open Db.RteGen in
- let register_getter fctref fct =
- Db.register fctref (fun () -> fct)
- in
- register_getter get_signedOv_status Signed_overflow.accessor;
- register_getter get_divMod_status Div_mod.accessor;
- register_getter get_initialized_status Initialized.accessor;
- register_getter get_signed_downCast_status Signed_downcast.accessor;
- register_getter get_memAccess_status Mem_access.accessor;
- register_getter get_pointerCall_status Pointer_call.accessor;
- register_getter get_unsignedOv_status Unsigned_overflow.accessor;
- register_getter get_unsignedDownCast_status Unsigned_downcast.accessor;
- register_getter get_pointer_downcast_status Pointer_downcast.accessor;
- register_getter get_float_to_int_status Float_to_int.accessor;
- register_getter get_finite_float_status Finite_float.accessor;
- register_getter get_pointer_value_status Pointer_value.accessor;
- register_getter get_bool_value_status Bool_value.accessor ;
- register_getter get_all_status all_statuses;
-;;
-
-(* dynamic registration *)
+let _ignore =
+ Dynamic.register
+ ~comment:"Generate all RTE annotations in the given function."
+ ~plugin:"RteGen"
+ "do_all_rte"
+ (Datatype.func Kernel_function.ty Datatype.unit)
+ Api.do_all_rte
-let _ =
+let _ignore =
Dynamic.register
~comment:"The emitter used for generating RTE annotations"
~plugin:"RteGen"
@@ -147,7 +81,7 @@ let main () =
if Options.Enabled.get () then begin
Options.feedback ~dkey:Options.dkey_annot ~level:2
"generating annotations";
- !Db.RteGen.compute ();
+ Api.compute ();
Options.feedback ~dkey:Options.dkey_annot ~level:2
"annotations computed"
end
diff --git a/src/plugins/slicing/gui/dune b/src/plugins/slicing/gui/dune
index ddc359106faec271bf503a990b59e01e7e6177ea..7726f1682dfb4e6f1eb5e6ff3ce1dcb6bb033155 100644
--- a/src/plugins/slicing/gui/dune
+++ b/src/plugins/slicing/gui/dune
@@ -20,6 +20,18 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Slicing GUI:" %{lib-available:frama-c-slicing.gui} "\n")
+ (echo " - Frama-C GUI:" %{lib-available:frama-c.gui} "\n")
+ (echo " - Slicing:" %{lib-available:frama-c-slicing.core} "\n")
+
+ )
+ )
+)
+
( library
(name slicing_gui)
(public_name frama-c-slicing.gui)
diff --git a/src/plugins/wp/gui/GuiSource.ml b/src/plugins/wp/gui/GuiSource.ml
index 79bfa4eb70814131d7b24302f180cba755c1b54f..69c8020583774dafba0ef2e42c13d38bb120f2f3 100644
--- a/src/plugins/wp/gui/GuiSource.ml
+++ b/src/plugins/wp/gui/GuiSource.ml
@@ -82,7 +82,7 @@ let kind_of_property = function
(* -------------------------------------------------------------------------- *)
let is_rte_generated kf =
- List.for_all (fun (_, _, lookup) -> lookup kf) (!Db.RteGen.get_all_status ())
+ List.for_all (fun (_, _, lookup) -> lookup kf) (RteGen.Api.get_all_status ())
class popup () =
object(self)
diff --git a/src/plugins/wp/gui/dune b/src/plugins/wp/gui/dune
index d6d53e011c0e1498e61363db7808ac19e8bbeb30..b3b7ce9ad83aa5bf0fd9a5e05305bbc9897630e7 100644
--- a/src/plugins/wp/gui/dune
+++ b/src/plugins/wp/gui/dune
@@ -25,7 +25,7 @@
(public_name frama-c-wp.gui)
(optional)
(flags -open Frama_c_kernel -open Frama_c_gui -open Wp :standard -w -9)
- (libraries frama-c-wp.core frama-c.kernel frama-c.gui why3 qed)
+ (libraries frama-c-wp.core frama-c.kernel frama-c-rtegen frama-c.gui why3 qed)
)
(plugin (optional) (name wp-gui) (libraries frama-c-wp.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 19c82da02da5fe950afdfd7423534289a576f0f0..acde1d77db3abfe5a4ec3798690483864ca6c79c 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -27,7 +27,7 @@ type t = {
cint : bool ;
kernel : (unit -> bool) ;
option : string ;
- status : (unit -> Db.RteGen.status_accessor) ref ;
+ status : unit -> RteGen.Api.status_accessor ;
}
let option name =
@@ -36,9 +36,9 @@ let option name =
let status db kf =
try
- (* Absolutely forbidden to use 'set' from Db.RteGen :
+ (* Absolutely forbidden to use 'set' from RteGen.Api :
this disables the generation of the associated RTE. *)
- let (_,_,get) = (!db) () in get kf
+ let (_,_,get) = db () in get kf
with Failure _ ->
Wp_parameters.warning ~once:true
"Missing RTE plug-in: can not generate conditions" ;
@@ -74,33 +74,33 @@ let generator =
[
{ name = "memory access" ;
kernel = always ; option = "-rte-mem" ; cint = false ;
- status = Db.RteGen.get_memAccess_status } ;
+ status = RteGen.Api.get_memAccess_status } ;
{ name = "division by zero" ;
kernel = always ; option = "-rte-div" ; cint = false ;
- status = Db.RteGen.get_divMod_status } ;
+ status = RteGen.Api.get_divMod_status } ;
{ name = "signed overflow" ; cint = true ;
kernel = Kernel.SignedOverflow.get ; option = "" ;
- status = Db.RteGen.get_signedOv_status } ;
+ status = RteGen.Api.get_signedOv_status } ;
{ name = "unsigned overflow" ; cint = true ;
kernel = Kernel.UnsignedOverflow.get ; option = "" ;
- status = Db.RteGen.get_unsignedOv_status } ;
+ status = RteGen.Api.get_unsignedOv_status } ;
{ name = "signed downcast" ; cint = true ; option = "" ;
kernel = Kernel.SignedDowncast.get ;
- status = Db.RteGen.get_signed_downCast_status } ;
+ status = RteGen.Api.get_signed_downCast_status } ;
{ name = "unsigned downcast" ; cint = true ; option = "" ;
kernel = Kernel.UnsignedDowncast.get ;
- status = Db.RteGen.get_unsignedDownCast_status } ;
+ status = RteGen.Api.get_unsignedDownCast_status } ;
{ name = "invalid bool value" ; cint = false ;
option = "-warn-invalid-bool" ;
kernel = Kernel.InvalidBool.get ;
- status = Db.RteGen.get_bool_value_status } ;
+ status = RteGen.Api.get_bool_value_status } ;
]
let generate model kf =
let update = ref false in
let cint = WpContext.on_context (model,WpContext.Kf kf) Cint.current () in
List.iter (configure ~update ~generate:true kf cint) generator ;
- if !update then !Db.RteGen.annotate_kf kf
+ if !update then RteGen.Api.annotate_kf kf
let generate_all model =
Wp_parameters.iter_kf (generate model)
diff --git a/tests/rte/compute_annot.ml b/tests/rte/compute_annot.ml
index 4ae1c287163e1fb7ffd7e8f924eda11192cfe982..7ef362bb5864a62627fc589a2ee7e243e68b9e62 100644
--- a/tests/rte/compute_annot.ml
+++ b/tests/rte/compute_annot.ml
@@ -4,7 +4,7 @@ let print () =
let print_status () =
Kernel.log "printing status";
- let _, _, get_signedOv_status = !Db.RteGen.get_signedOv_status () in
+ let _, _, get_signedOv_status = RteGen.Api.get_signedOv_status () in
Globals.Functions.iter
(fun kf ->
Kernel.log "kf = %s rte_gen_status = %b\n"
@@ -23,7 +23,7 @@ let main () =
Kernel.log "computing rte-div annotations" ;
Dynamic.Parameter.Bool.set "-rte-div" true ;
- !Db.RteGen.compute () ;
+ RteGen.Api.compute () ;
print ();
print_status ();
@@ -34,7 +34,7 @@ let main () =
| _ -> false
in
Alarms.remove ~filter emitter;
- !Db.RteGen.compute () ;
+ RteGen.Api.compute () ;
print ();
print_status ()
diff --git a/tests/rte/my_annot_proxy.ml b/tests/rte/my_annot_proxy.ml
index f4c4b44f5f61b9657d327fd751f50ceee62adcd6..cd22de24d55aeb20304ac0c9c47cac5a00854a52 100644
--- a/tests/rte/my_annot_proxy.ml
+++ b/tests/rte/my_annot_proxy.ml
@@ -4,7 +4,7 @@ let print () =
let print_status () =
Kernel.log "printing status";
- let rte_state_getter_list = !Db.RteGen.get_all_status () in
+ let rte_state_getter_list = RteGen.Api.get_all_status () in
Globals.Functions.iter
(fun kf ->
Kernel.log "kf = %s" (Kernel_function.get_name kf) ;
@@ -23,7 +23,7 @@ let main () =
if not(Ast.is_computed ()) then Ast.compute () ;
print ();
- Globals.Functions.iter (fun kf -> !Db.RteGen.annotate_kf kf);
+ Globals.Functions.iter (fun kf -> RteGen.Api.annotate_kf kf);
print () ;
print_status ();
diff --git a/tests/rte/my_annotation.ml b/tests/rte/my_annotation.ml
index 1aff9c30ecbb73fa398f28109665cc76c5d38686..c1549b692964c6eb2732665b2848d4cb38f28a61 100644
--- a/tests/rte/my_annotation.ml
+++ b/tests/rte/my_annotation.ml
@@ -4,7 +4,7 @@ let print () =
let print_status () =
Kernel.log "printing status";
- let _, _, get_signedOv_status = !Db.RteGen.get_signedOv_status () in
+ let _, _, get_signedOv_status = RteGen.Api.get_signedOv_status () in
Globals.Functions.iter
(fun kf ->
Kernel.log "kf = %s rte_gen_status = %b\n"
@@ -22,12 +22,12 @@ let main () =
if not(Ast.is_computed ()) then Ast.compute () ;
print ();
- Globals.Functions.iter (fun kf -> !Db.RteGen.annotate_kf kf);
+ Globals.Functions.iter (fun kf -> RteGen.Api.annotate_kf kf);
print () ;
print_status ();
Kernel.log "Removing some rte annotations" ;
- let _, set_signed, _ = !Db.RteGen.get_signedOv_status () in
+ let _, set_signed, _ = RteGen.Api.get_signedOv_status () in
let emitter = Dynamic.get ~plugin:"RteGen" "emitter" Emitter.ty in
let filter = function
| Alarms.Overflow _ -> true
@@ -43,7 +43,7 @@ let main () =
(fun kf ->
if !one_on_two then begin
set_signed kf false;
- !Db.RteGen.annotate_kf kf
+ RteGen.Api.annotate_kf kf
end;
one_on_two := not !one_on_two);
print () ;
diff --git a/tests/rte/rte_get_annot.ml b/tests/rte/rte_get_annot.ml
index da89041557ec72d35613ba6ece2094df6b7773e8..c360664de0dccaa55c8c903489869ccae5dba7d7 100644
--- a/tests/rte/rte_get_annot.ml
+++ b/tests/rte/rte_get_annot.ml
@@ -48,7 +48,7 @@ let show_rte_of_kf kf =
let main () =
Ast.compute () ;
Kernel.SignedOverflow.on ();
- let do_rte = !Db.RteGen.do_rte in
+ let do_rte = RteGen.Api.do_rte in
Globals.Functions.iter (fun kf -> do_rte kf);
print () ;
Globals.Functions.iter show_rte_of_kf