From fd973425de1c53a306e051038d5430fae9c4e427 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 12 Oct 2022 10:39:20 +0200
Subject: [PATCH] [E-ACSL] prepare for future RteGen as optional dependence
---
src/plugins/e-acsl/src/analyses/rte.ml | 39 ++++---------------------
src/plugins/e-acsl/src/analyses/rte.mli | 4 +++
src/plugins/e-acsl/src/main.ml | 2 +-
3 files changed, 11 insertions(+), 34 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/rte.ml b/src/plugins/e-acsl/src/analyses/rte.ml
index f542d1fee0f..a800c436701 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 f4697989d10..93271568009 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/main.ml b/src/plugins/e-acsl/src/main.ml
index 3849fbc9fb4..54342436cdf 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 RteGen.Api.self)
+ (Rte.get_state_selection_with_dependencies ())
(State_selection.with_dependencies Options.Run.self)
in
Project.clear ~selection ~project:copied_prj ();
--
GitLab