From 714a13d3da80f372d8ed16174e91fe01972edf12 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 8 Nov 2019 14:57:46 +0100
Subject: [PATCH] [test] test case for reported issue
---
tests/spec/extend_extern.i | 7 +++++++
tests/spec/extend_extern.ml | 22 ++++++++++++++++++++++
2 files changed, 29 insertions(+)
create mode 100644 tests/spec/extend_extern.i
create mode 100644 tests/spec/extend_extern.ml
diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
new file mode 100644
index 00000000000..8dffe226177
--- /dev/null
+++ b/tests/spec/extend_extern.i
@@ -0,0 +1,7 @@
+/* run.config
+ MACRO: PTEST_MAKE_MODULE make FRAMAC_USER_OFLAGS="-package why3" FRAMAC_USER_BFLAGS="-package why3"
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT:
+ */
+/*@ predicate load(char * x) = \true ; */
+/*@ why3 load("List"); */
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
new file mode 100644
index 00000000000..70f1ad660c2
--- /dev/null
+++ b/tests/spec/extend_extern.ml
@@ -0,0 +1,22 @@
+open Logic_typing
+open Cil_types
+
+let load_theory = function
+ | { pred_content = Papp (_, [], [ { term_node = TConst(LStr _name) } ] ) } ->
+ let open Why3 in ignore (
+ Theory.import_namespace Theory.empty_ns [_name]
+ )
+ | _ -> assert false
+
+let typing ~typing_context ~loc lexprs =
+ ignore loc ;
+ let type_predicate =
+ typing_context.type_predicate typing_context (Lenv.empty ())
+ in
+ let predicates = List.map type_predicate lexprs in
+ List.iter load_theory predicates ;
+ Ext_preds predicates
+
+
+let () =
+ Logic_typing.register_global_extension "why3" false typing
--
GitLab