From e5faf9399981ee39799a64bb5d2da9a78a808cb4 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 29 Sep 2020 09:32:09 +0200
Subject: [PATCH] [eacsl:runtime] Merge RTL pragmas into the user's AST
---
src/plugins/e-acsl/src/project_initializer/rtl.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index ee6ea93f43a..07be50d1a64 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -156,8 +156,10 @@ let lookup_rtl_globals rtl_ast =
| GAnnot _ :: l ->
(* ignoring annotations from the AST *)
do_globals acc l
- | GAsm _ | GPragma _ | GText _ as g :: _l ->
- Kernel.fatal "unexpected global %a" Printer.pp_global g
+ | GPragma _ as g :: l ->
+ do_it Symbols.mem_global acc l g
+ | GAsm _ | GText _ as g :: _l ->
+ Options.fatal "unexpected global %a" Printer.pp_global g
in
do_globals [] rtl_ast.globals
@@ -245,8 +247,10 @@ let insert_rtl_globals rtl_prj rtl_globals ast =
acc
in
add acc l
- | GAnnot _ | GAsm _ | GPragma _ | GText _ as g :: _l ->
- Kernel.fatal "unexpected global %a" Printer.pp_global g
+ | GPragma _ as g :: l ->
+ add (g :: acc) l
+ | GAnnot _ | GAsm _ | GText _ as g :: _l ->
+ Options.fatal "unexpected global %a" Printer.pp_global g
in
ast.globals <- add ast.globals rtl_globals
--
GitLab