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/main.ml b/src/plugins/e-acsl/src/main.ml index 3849fbc9fb41a45b8efa03220a62878b6250c407..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 RteGen.Api.self) + (Rte.get_state_selection_with_dependencies ()) (State_selection.with_dependencies Options.Run.self) in Project.clear ~selection ~project:copied_prj ();