[E-ACSL] prepare for future RteGen as optional dependence

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/main.ml

@@ -77,7 +77,7 @@ let generate_code =
                redoing the RTE management system  *)
             let selection =
               State_selection.union
-                (State_selection.with_dependencies RteGen.Api.self)
+                (Rte.get_state_selection_with_dependencies ())
                 (State_selection.with_dependencies Options.Run.self)
             in
             Project.clear ~selection ~project:copied_prj ();