Merge branch 'feature/patrick/removes-rte-from-db' into 'master'

[RteGen] removes RteGen from Db

See merge request frama-c/frama-c!3916

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
 

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

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:

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 ../../../../.."

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)))
 

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 ();

src/plugins/gui/design.mli

@@ -277,8 +277,6 @@ sig
 
 end
 
-
-
 (*
 Local Variables:
 compile-command: "make -C ../../.."

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")
   )
   )
 )

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

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:

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

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

src/plugins/rte/api.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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)

src/plugins/rte/api.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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)
 )

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
 

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 ../../.."

src/plugins/rte/gui/dune

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  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)))

src/plugins/rte/gui/rtegen_gui.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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