From d788d610096c0440ea157b4acddf69cdb97acc59 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 6 Aug 2020 11:28:58 +0200
Subject: [PATCH] [eacsl] Add a way to filter generated RTE annotations

---
 src/plugins/e-acsl/src/code_generator/translate.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 22d5bef727c..b7d70865560 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1040,9 +1040,14 @@ and translate_rte_annots:
   is_visiting_valid := old_valid;
   Env.set_annotation_kind env old_kind
 
-and translate_rte kf env e =
+and translate_rte ?filter kf env e =
   let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
   let l = Rte.exp kf stmt e in
+  let l =
+    match filter with
+    | Some f -> List.filter f l
+    | None -> l
+  in
   translate_rte_annots Printer.pp_exp e kf env l
 
 and translate_named_predicate kf env p =
-- 
GitLab