From 6771e68115bb816845b44f04eb8f5c01387dce65 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 19 Sep 2024 13:22:41 +0200
Subject: [PATCH] [tests] Add tests for the \plugin:: syntax for import
---
tests/spec/Extend_conflict.i | 10 ----
tests/spec/Extend_errors.c | 40 +++++++++++++
tests/spec/Extend_errors.ml | 51 +++++++++++++++++
tests/spec/Extend_kernel.i | 13 -----
tests/spec/Extend_plugin.ml | 22 --------
tests/spec/Extend_recursive_preprocess.ml | 12 ++--
tests/spec/Extend_type_token.i | 10 ----
tests/spec/Extend_warning.i | 12 ----
tests/spec/import.i | 25 ++++++---
tests/spec/import_errors.c | 46 +++++++++++++++
tests/spec/module.c | 17 +++++-
tests/spec/oracle/Extend_conflict.res.oracle | 6 --
tests/spec/oracle/Extend_errors.0.res.oracle | 43 ++++++++++++++
tests/spec/oracle/Extend_errors.1.res.oracle | 11 ++++
tests/spec/oracle/Extend_errors.2.res.oracle | 13 +++++
tests/spec/oracle/Extend_errors.3.res.oracle | 8 +++
tests/spec/oracle/Extend_errors.4.res.oracle | 6 ++
tests/spec/oracle/Extend_kernel.res.oracle | 4 --
.../spec/oracle/Extend_type_token.res.oracle | 6 --
tests/spec/oracle/Extend_warning.res.oracle | 15 -----
tests/spec/oracle/import.0.res.oracle | 33 ++++++++++-
tests/spec/oracle/import.1.res.oracle | 56 ++++++++++++++++---
tests/spec/oracle/import_errors.0.res.oracle | 43 ++++++++++++++
tests/spec/oracle/import_errors.1.res.oracle | 6 ++
tests/spec/oracle/import_errors.2.res.oracle | 6 ++
tests/spec/oracle/import_errors.3.res.oracle | 6 ++
tests/spec/oracle/module.1.res.oracle | 4 ++
tests/spec/{import.ml => test_import.ml} | 26 +++++++--
28 files changed, 423 insertions(+), 127 deletions(-)
delete mode 100644 tests/spec/Extend_conflict.i
create mode 100644 tests/spec/Extend_errors.c
create mode 100644 tests/spec/Extend_errors.ml
delete mode 100644 tests/spec/Extend_kernel.i
delete mode 100644 tests/spec/Extend_plugin.ml
delete mode 100644 tests/spec/Extend_type_token.i
delete mode 100644 tests/spec/Extend_warning.i
create mode 100644 tests/spec/import_errors.c
delete mode 100644 tests/spec/oracle/Extend_conflict.res.oracle
create mode 100644 tests/spec/oracle/Extend_errors.0.res.oracle
create mode 100644 tests/spec/oracle/Extend_errors.1.res.oracle
create mode 100644 tests/spec/oracle/Extend_errors.2.res.oracle
create mode 100644 tests/spec/oracle/Extend_errors.3.res.oracle
create mode 100644 tests/spec/oracle/Extend_errors.4.res.oracle
delete mode 100644 tests/spec/oracle/Extend_kernel.res.oracle
delete mode 100644 tests/spec/oracle/Extend_type_token.res.oracle
delete mode 100644 tests/spec/oracle/Extend_warning.res.oracle
create mode 100644 tests/spec/oracle/import_errors.0.res.oracle
create mode 100644 tests/spec/oracle/import_errors.1.res.oracle
create mode 100644 tests/spec/oracle/import_errors.2.res.oracle
create mode 100644 tests/spec/oracle/import_errors.3.res.oracle
rename tests/spec/{import.ml => test_import.ml} (51%)
diff --git a/tests/spec/Extend_conflict.i b/tests/spec/Extend_conflict.i
deleted file mode 100644
index cb82bc29c44..00000000000
--- a/tests/spec/Extend_conflict.i
+++ /dev/null
@@ -1,10 +0,0 @@
-/* run.config
- MODULE: Extend_plugin
- EXIT: 1
- STDOPT:
-*/
-
-//@ \eva::foo x == 0;
-int g(int x) {
- return x;
-}
diff --git a/tests/spec/Extend_errors.c b/tests/spec/Extend_errors.c
new file mode 100644
index 00000000000..775c3bff98e
--- /dev/null
+++ b/tests/spec/Extend_errors.c
@@ -0,0 +1,40 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ COMMENT: Debug is set to distinguish this particular test in the module
+ STDOPT: +"-debug 1 -kernel-msg-key acsl-extension"
+ STDOPT: +"-cpp-extra-args=-DWARN_EXT_KERNEL"
+ STDOPT: +"-cpp-extra-args=-DWARN_EXT_TOKEN"
+ EXIT: 1
+ STDOPT: +"-cpp-extra-args=-DWARN_EXT_UNKNOWN"
+ STDOPT: +"-cpp-extra-args=-DERR_EXT_AMBIGUITY"
+*/
+
+/*@ \myplugin1::foo x == 0;
+ \myplugin2::foo x == 0;
+*/
+int ok(int x) {
+ return x;
+}
+
+// Using a token as extension name
+#ifdef WARN_EXT_TOKEN
+//@ \myplugin1::__FC_FILENAME__ x == 0;
+#endif
+
+#ifdef ERR_EXT_KERNEL
+int kernel(int x) {
+ //@ \kernel::calls ok;
+ return ok(x);
+}
+#endif
+
+#ifdef WARN_EXT_UNKNOWN
+/*@ \myplugin1::bar x == 0;
+ \unknown_plugin::bar x == 0;
+ */
+#endif
+
+// Using an extension registered 2 times or more with different plugins
+#ifdef ERR_EXT_AMBIGUITY
+//@ foo x == 0;
+#endif
diff --git a/tests/spec/Extend_errors.ml b/tests/spec/Extend_errors.ml
new file mode 100644
index 00000000000..9a4d583747e
--- /dev/null
+++ b/tests/spec/Extend_errors.ml
@@ -0,0 +1,51 @@
+open Logic_typing
+
+module Plugin1 =
+ Plugin.Register
+ (struct
+ let name = "MyPlugin1"
+ let shortname = "myplugin1"
+ let help = ""
+ end)
+
+module Plugin2 =
+ Plugin.Register
+ (struct
+ let name = "MyPlugin2"
+ let shortname = "myplugin2"
+ let help = ""
+ end)
+
+let type_foo typing_context _loc l =
+ let preds =
+ List.map
+ (typing_context.type_predicate
+ typing_context typing_context.pre_state)
+ l
+ in
+ Cil_types.Ext_preds preds
+
+let catch msg f x =
+ try
+ Kernel.feedback "Triggering %s :" msg;
+ ignore(f x)
+ with _ -> ()
+
+let cover_errors () =
+ catch "User Error" (Logic_env.is_extension ~plugin:None) "foo";
+ catch "Unsupported" (Logic_env.preprocess_extension ~plugin:(Some "myplugin1")) "bar"
+
+let cover_warnings () =
+ Acsl_extension.register_behavior ~plugin:"myplugin1" "foo" type_foo false;
+ Acsl_extension.register_behavior ~plugin:"myplugin1" "unfold" type_foo false
+
+let () =
+ Format.printf "[test-extend_errors] Linking.@.";
+ Acsl_extension.register_behavior ~plugin:"myplugin1" "foo" type_foo false;
+ Acsl_extension.register_behavior ~plugin:"myplugin2" "foo" type_foo false;
+ Acsl_extension.register_behavior ~plugin:"myplugin2" "bar" type_foo false;
+
+ if Kernel.GeneralDebug.get () = 1 then begin
+ cover_warnings ();
+ cover_errors ()
+ end
diff --git a/tests/spec/Extend_kernel.i b/tests/spec/Extend_kernel.i
deleted file mode 100644
index a53a4fe67fd..00000000000
--- a/tests/spec/Extend_kernel.i
+++ /dev/null
@@ -1,13 +0,0 @@
-/* run.config
- EXIT: 1
- STDOPT:
-*/
-
-int g(int x){
- return x + 42;
-}
-
-int f(int x) {
- //@ \kernel::calls g;
- return g(x);
-}
diff --git a/tests/spec/Extend_plugin.ml b/tests/spec/Extend_plugin.ml
deleted file mode 100644
index 0a826d29688..00000000000
--- a/tests/spec/Extend_plugin.ml
+++ /dev/null
@@ -1,22 +0,0 @@
-open Logic_typing
-
-include
- Plugin.Register
- (struct
- let name = "MyPlugin"
- let shortname = "myplugin"
- let help = ""
- end)
-
-let type_foo typing_context _loc l =
- let preds =
- List.map
- (typing_context.type_predicate
- typing_context typing_context.pre_state)
- l
- in
- Cil_types.Ext_preds preds
-
-let () =
- Acsl_extension.register_behavior ~plugin:"myplugin" "foo" type_foo false;
- Acsl_extension.register_behavior ~plugin:"myplugin" "foo" type_foo false
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index 7a836e0d105..be862c32953 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -12,12 +12,12 @@ let ext_typing_fooo _typing_context _loc l =
let ext_typing_block typing_context loc_here node =
match node.extended_node with
- | Ext_lexpr (name,data) ->
- let status,kind = Logic_typing.get_typer name ~typing_context ~loc:node.extended_loc data in
- Logic_const.new_acsl_extension name loc_here status kind
- | Ext_extension (name, id, data) ->
- let status,kind = Logic_typing.get_typer_block name ~typing_context ~loc:node.extended_loc (id,data) in
- Logic_const.new_acsl_extension name loc_here status kind
+ | Ext_lexpr (name,plugin,data) ->
+ let status,kind = Logic_typing.get_typer ~plugin name ~typing_context ~loc:node.extended_loc data in
+ Logic_const.new_acsl_extension name plugin loc_here status kind
+ | Ext_extension (name, plugin, id, data) ->
+ let status,kind = Logic_typing.get_typer_block ~plugin name ~typing_context ~loc:node.extended_loc (id,data) in
+ Logic_const.new_acsl_extension name plugin loc_here status kind
let ext_typing_foo typing_context loc (s,d) =
let block = List.map (ext_typing_block typing_context loc) d in
diff --git a/tests/spec/Extend_type_token.i b/tests/spec/Extend_type_token.i
deleted file mode 100644
index 938a1551d68..00000000000
--- a/tests/spec/Extend_type_token.i
+++ /dev/null
@@ -1,10 +0,0 @@
-/* run.config
- MODULE: Extend_plugin
- EXIT: 1
- STDOPT:
-*/
-
-//@ \myplugin::integer x == 0;
-int g(int x) {
- return x;
-}
diff --git a/tests/spec/Extend_warning.i b/tests/spec/Extend_warning.i
deleted file mode 100644
index a1773b04cdc..00000000000
--- a/tests/spec/Extend_warning.i
+++ /dev/null
@@ -1,12 +0,0 @@
-/* run.config
- MODULE: Extend_plugin
- STDOPT: +"-kernel-warn-key=extension-unknown=active"
-*/
-
-/*@ \myplugin::foo x == 0;
- \myplugin::bar x == 0;
- \unknown_plugin::bar x == 0;
- */
-int f(int x) {
- return x;
-}
diff --git a/tests/spec/import.i b/tests/spec/import.i
index 837dffbac76..0644f8f3da6 100644
--- a/tests/spec/import.i
+++ b/tests/spec/import.i
@@ -1,13 +1,20 @@
/* run.config
-MODULE: @PTEST_NAME@
-OPT: -print
-OPT: -print -kernel-msg-key printer:imported-modules
+ MODULE: Test_import
+ STDOPT: +"-kernel-msg-key acsl-extension"
+ STDOPT: +"-kernel-msg-key acsl-extension -kernel-msg-key printer:imported-modules"
*/
-/*@ import foo: A::B; */
-/*@ predicate check1(B::t x) = B::check(x,0); */
-/*@ predicate check2(A::B::t x) = A::B::check(x,0); */
+//@ import \myplugin1::foo: A::B;
+//@ predicate check1(B::t x) = B::check(x,0);
+//@ predicate check2(A::B::t x) = A::B::check(x,0);
-/*@ import foo: A::B \as C; */
-/*@ predicate check3(C::t x) = C::check(x,0); */
-/*@ predicate check4(C::t x) = A::B::check(x,0); */
+//@ import \myplugin1::foo: A::B \as C;
+//@ predicate check3(C::t x) = C::check(x,0);
+//@ predicate check4(C::t x) = A::B::check(x,0);
+
+//@ import \myplugin2::foo: X;
+//@ predicate check5(X::t x) = X::check(x,0);
+
+//@ import bar: X::Y;
+//@ predicate check6(Y::t x) = Y::check(x,0);
+//@ predicate check7(X::Y::t x) = X::Y::check(x,0);
diff --git a/tests/spec/import_errors.c b/tests/spec/import_errors.c
new file mode 100644
index 00000000000..24148525425
--- /dev/null
+++ b/tests/spec/import_errors.c
@@ -0,0 +1,46 @@
+/* run.config
+ MODULE: Test_import
+ COMMENT: Debug is set to distinguish this particular test in the module
+ STDOPT: +"-debug 1 -kernel-msg-key acsl-extension -cpp-extra-args=-DWARNINGS"
+ EXIT: 1
+ STDOPT: +"-cpp-extra-args=-DERR_DRIVER_AMBIGUITY"
+ STDOPT: +"-cpp-extra-args=-DERR_UNKNOWN_DRIVER1"
+ STDOPT: +"-cpp-extra-args=-DERR_UNKNOWN_DRIVER2"
+*/
+
+#ifdef WARNINGS
+// Wrong token identifier (here parsed as BEHAVIORS)
+//@ import \myplugin1::behaviors: A;
+
+//@ import \myplugin1::foo: B;
+
+// Silently ignored, duplicated import
+//@ import \myplugin1::foo: B;
+
+// Already imported with different driver
+//@ import \myplugin1::bar: B;
+// Already imported with different plugin
+//@ import \myplugin2::foo: B;
+
+/*@
+ module C {
+ type t;
+ predicate check(t x, ℤ k) ;
+ }
+ // Module C already defined
+ import \myplugin1::foo: C;
+*/
+#endif
+
+#ifdef ERR_DRIVER_AMBIGUITY
+//@ import foo: A::B \as D;
+#endif
+
+#ifdef ERR_UNKNOWN_DRIVER1
+//@ import \myplugin1::toto: E;
+#endif
+
+#ifdef ERR_UNKNOWN_DRIVER2
+//@ import toto: F;
+#endif
+
diff --git a/tests/spec/module.c b/tests/spec/module.c
index 6fa3d132da5..2c2d027f58c 100644
--- a/tests/spec/module.c
+++ b/tests/spec/module.c
@@ -81,6 +81,21 @@ logic integer z = b::a; // KO
import foo::jazz ;
logic a f_ko(a x) = bar::f(x); // KO, ill typed
}
- */
+*/
+/*@
+ // Duplicated module
+ module Foo {
+ type t;
+ }
+*/
+
+/*@
+ // Nested module in axiomatix is not supported yet
+ axiomatic p {
+ module Bar {
+ type t;
+ }
+ }
+*/
#endif
diff --git a/tests/spec/oracle/Extend_conflict.res.oracle b/tests/spec/oracle/Extend_conflict.res.oracle
deleted file mode 100644
index ae562310f5f..00000000000
--- a/tests/spec/oracle/Extend_conflict.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-[kernel:acsl-extension] Warning:
- Trying to register ACSL extension foo twice. Ignoring second extension
-[kernel] Parsing Extend_conflict.i (no preprocessing)
-[kernel] Extend_conflict.i:7: User Error:
- Extension 'foo' is from myplugin and not eva
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_errors.0.res.oracle b/tests/spec/oracle/Extend_errors.0.res.oracle
new file mode 100644
index 00000000000..1cd048aac04
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.0.res.oracle
@@ -0,0 +1,43 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
+[test-extend_errors] Linking.
+[kernel:acsl-extension] Registering acsl extension \myplugin1::foo
+[kernel:acsl-extension] Registering acsl extension \myplugin2::foo
+[kernel:acsl-extension] Registering acsl extension \myplugin2::bar
+[kernel:acsl-extension] Registering acsl extension \myplugin1::foo
+[kernel:acsl-extension] Warning:
+ Trying to register ACSL extension foo twice with plugin myplugin1. Ignoring the second extension
+[kernel:acsl-extension] Registering acsl extension \myplugin1::unfold
+[kernel:acsl-extension] Warning:
+ Trying to register ACSL extension unfold reserved by frama-c. Rename this extension to avoid conflict with the kernel. Ignored extension
+[kernel] Triggering User Error :
+[kernel] <unknown location> User Error:
+ Conflicts on extension named 'foo' registered by different plugins (myplugin2,
+ myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
+[kernel] Triggering Unsupported :
+[kernel] <unknown location> Failure:
+ Unsupported clause extension named '\myplugin1::bar'
+[kernel] Parsing Extend_errors.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ \myplugin1::foo x ≡ 0;
+ \myplugin2::foo x ≡ 0; */
+int ok(int x)
+{
+ /* sid:2 */
+ return x;
+}
+
+
diff --git a/tests/spec/oracle/Extend_errors.1.res.oracle b/tests/spec/oracle/Extend_errors.1.res.oracle
new file mode 100644
index 00000000000..cc45c5f9245
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.1.res.oracle
@@ -0,0 +1,11 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ \myplugin1::foo x ≡ 0;
+ \myplugin2::foo x ≡ 0; */
+int ok(int x)
+{
+ return x;
+}
+
+
diff --git a/tests/spec/oracle/Extend_errors.2.res.oracle b/tests/spec/oracle/Extend_errors.2.res.oracle
new file mode 100644
index 00000000000..27de177ede1
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.2.res.oracle
@@ -0,0 +1,13 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+[kernel:annot-error] Extend_errors.c:21: Warning:
+ unexpected token '\myplugin1::__FC_FILENAME__'
+/* Generated by Frama-C */
+/*@ \myplugin1::foo x ≡ 0;
+ \myplugin2::foo x ≡ 0; */
+int ok(int x)
+{
+ return x;
+}
+
+
diff --git a/tests/spec/oracle/Extend_errors.3.res.oracle b/tests/spec/oracle/Extend_errors.3.res.oracle
new file mode 100644
index 00000000000..c12d7dc67ef
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.3.res.oracle
@@ -0,0 +1,8 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+[kernel:extension-unknown] Extend_errors.c:32: Warning:
+ Ignoring unregistered extension 'bar' of plug-in myplugin1
+[kernel:plugin-not-loaded] Extend_errors.c:33: Warning:
+ Ignoring extension 'bar' for unloaded plug-in unknown_plugin
+[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_errors.4.res.oracle b/tests/spec/oracle/Extend_errors.4.res.oracle
new file mode 100644
index 00000000000..62c309ecec0
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.4.res.oracle
@@ -0,0 +1,6 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+[kernel] Extend_errors.c:39: User Error:
+ Conflicts on extension named 'foo' registered by different plugins (myplugin2,
+ myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_kernel.res.oracle b/tests/spec/oracle/Extend_kernel.res.oracle
deleted file mode 100644
index 80c8ec0df28..00000000000
--- a/tests/spec/oracle/Extend_kernel.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing Extend_kernel.i (no preprocessing)
-[kernel] Extend_kernel.i:11: User Error:
- Extension 'calls' from frama-c's kernel should not be used with the syntax \kernel::calls
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_type_token.res.oracle b/tests/spec/oracle/Extend_type_token.res.oracle
deleted file mode 100644
index b14752a485d..00000000000
--- a/tests/spec/oracle/Extend_type_token.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-[kernel:acsl-extension] Warning:
- Trying to register ACSL extension foo twice. Ignoring second extension
-[kernel] Parsing Extend_type_token.i (no preprocessing)
-[kernel] Extend_type_token.i:7: User Error:
- Type token 'integer' received instead of extension identifier
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_warning.res.oracle b/tests/spec/oracle/Extend_warning.res.oracle
deleted file mode 100644
index 9ba50241a67..00000000000
--- a/tests/spec/oracle/Extend_warning.res.oracle
+++ /dev/null
@@ -1,15 +0,0 @@
-[kernel:acsl-extension] Warning:
- Trying to register ACSL extension foo twice. Ignoring second extension
-[kernel] Parsing Extend_warning.i (no preprocessing)
-[kernel:extension-unknown] Extend_warning.i:7: Warning:
- Ignoring unregistered extension 'bar' of plug-in myplugin
-[kernel:plugin-not-loaded] Extend_warning.i:8: Warning:
- Ignoring extension 'bar' for unloaded plug-in unknown_plugin
-/* Generated by Frama-C */
-/*@ \myplugin::foo x ≡ 0; */
-int f(int x)
-{
- return x;
-}
-
-
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
index f0f5707e2ba..4f812b2f7f0 100644
--- a/tests/spec/oracle/import.0.res.oracle
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -1,9 +1,28 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
[test-import] Linking.
-[test-import] Registering 'foo'.
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::bar
+[kernel:acsl-extension] Registering importer extension \myplugin2::foo
[kernel] Parsing import.i (no preprocessing)
[test-import:7] Loading A::B.
+[test-import:15] Loading X.
+[test-import:18] Loading X::Y.
/* Generated by Frama-C */
-/*@ import foo: A::B \as _ ;
+/*@ import \myplugin1::foo: A::B \as _ ;
*/
/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
*/
@@ -13,4 +32,14 @@
*/
/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
*/
+/*@ import \myplugin2::foo: X \as _ ;
+ */
+/*@ predicate check5(X::t x) = X::check(x, 0);
+ */
+/*@ import bar: X::Y \as _ ;
+ */
+/*@ predicate check6(X::Y::t x) = X::Y::check(x, 0);
+ */
+/*@ predicate check7(X::Y::t x) = X::Y::check(x, 0);
+ */
diff --git a/tests/spec/oracle/import.1.res.oracle b/tests/spec/oracle/import.1.res.oracle
index b5236c1c99d..51394dba248 100644
--- a/tests/spec/oracle/import.1.res.oracle
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -1,22 +1,64 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
[test-import] Linking.
-[test-import] Registering 'foo'.
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::bar
+[kernel:acsl-extension] Registering importer extension \myplugin2::foo
[kernel] Parsing import.i (no preprocessing)
[test-import:7] Loading A::B.
+[test-import:15] Loading X.
+[test-import:18] Loading X::Y.
/* Generated by Frama-C */
-/*@ // import foo:
- module A::B {
+/*@
+// import \myplugin1::foo:
+module A::B {
+ type t;
+
+ predicate check(t x, ℤ k) ;
+
+ }
+ */
+/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ // import \myplugin2::foo:
+ module X {
type t;
predicate check(t x, ℤ k) ;
}
*/
-/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+/*@ predicate check5(X::t x) = X::check(x, 0);
*/
-/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+/*@ // import bar:
+ module X::Y {
+ type t;
+
+ predicate check(t x, ℤ k) ;
+
+ }
*/
-/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+/*@ predicate check6(X::Y::t x) = X::Y::check(x, 0);
*/
-/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+/*@ predicate check7(X::Y::t x) = X::Y::check(x, 0);
*/
diff --git a/tests/spec/oracle/import_errors.0.res.oracle b/tests/spec/oracle/import_errors.0.res.oracle
new file mode 100644
index 00000000000..3b7826751f3
--- /dev/null
+++ b/tests/spec/oracle/import_errors.0.res.oracle
@@ -0,0 +1,43 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
+[test-import] Linking.
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::bar
+[kernel:acsl-extension] Registering importer extension \myplugin2::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Warning:
+ Trying to register importer extension foo twice with plugin myplugin1. Ignoring the second extension
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel:annot-error] import_errors.c:13: Warning:
+ unexpected token '\myplugin1::behaviors:'
+[test-import:15] Loading B.
+[kernel:annot-error] import_errors.c:21: Warning:
+ Module B already imported with driver \myplugin1::foo (at import_errors.c:15). Ignoring global annotation
+[kernel:annot-error] import_errors.c:23: Warning:
+ Module B already imported with driver \myplugin1::foo (at import_errors.c:15). Ignoring global annotation
+[kernel:annot-error] import_errors.c:31: Warning:
+ Module C already defined (at import_errors.c:26). Ignoring global annotation
+/* Generated by Frama-C */
+/*@ import \myplugin1::foo: B \as _ ;
+ */
+/*@ module C {
+ type t;
+
+ predicate check(t x, ℤ k) ;
+
+ }
+ */
+
diff --git a/tests/spec/oracle/import_errors.1.res.oracle b/tests/spec/oracle/import_errors.1.res.oracle
new file mode 100644
index 00000000000..e9fce01548f
--- /dev/null
+++ b/tests/spec/oracle/import_errors.1.res.oracle
@@ -0,0 +1,6 @@
+[test-import] Linking.
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel] import_errors.c:36: User Error:
+ Conflicts on extension named 'foo' registered by different plugins (myplugin2,
+ myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/import_errors.2.res.oracle b/tests/spec/oracle/import_errors.2.res.oracle
new file mode 100644
index 00000000000..5d38e6ba880
--- /dev/null
+++ b/tests/spec/oracle/import_errors.2.res.oracle
@@ -0,0 +1,6 @@
+[test-import] Linking.
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel:extension-unknown] import_errors.c:40: Warning:
+ Ignoring unregistered importer extension 'toto' of plug-in myplugin1
+[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/import_errors.3.res.oracle b/tests/spec/oracle/import_errors.3.res.oracle
new file mode 100644
index 00000000000..6d3621d8f3d
--- /dev/null
+++ b/tests/spec/oracle/import_errors.3.res.oracle
@@ -0,0 +1,6 @@
+[test-import] Linking.
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel:extension-unknown] import_errors.c:44: Warning:
+ Ignoring unregistered importer extension 'toto'
+[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/module.1.res.oracle b/tests/spec/oracle/module.1.res.oracle
index b59f47ec8ea..edccf24cec3 100644
--- a/tests/spec/oracle/module.1.res.oracle
+++ b/tests/spec/oracle/module.1.res.oracle
@@ -7,6 +7,10 @@
unbound logic variable b::a. Ignoring global annotation
[kernel:annot-error] module.c:82: Warning:
incompatible types foo::jazz::a and foo::bar::a. Ignoring global annotation
+[kernel:annot-error] module.c:88: Warning:
+ Duplicated module Foo (first occurrence at module.c:7). Ignoring global annotation
+[kernel:annot-error] module.c:96: Warning:
+ Nested module and axiomatic. Ignoring body of Bar. Ignoring global annotation
/* Generated by Frama-C */
/*@
module Foo {
diff --git a/tests/spec/import.ml b/tests/spec/test_import.ml
similarity index 51%
rename from tests/spec/import.ml
rename to tests/spec/test_import.ml
index ca99db7c984..08eb2eab11d 100644
--- a/tests/spec/import.ml
+++ b/tests/spec/test_import.ml
@@ -1,6 +1,23 @@
open Cil_types
open Logic_typing
+
+module Plugin1 =
+ Plugin.Register
+ (struct
+ let name = "MyPlugin1"
+ let shortname = "myplugin1"
+ let help = ""
+ end)
+
+module Plugin2 =
+ Plugin.Register
+ (struct
+ let name = "MyPlugin2"
+ let shortname = "myplugin2"
+ let help = ""
+ end)
+
let () = Format.printf "[test-import] Linking.@."
let loader (ctxt: module_builder) (loc: location) (m: string list) =
@@ -17,9 +34,10 @@ let loader (ctxt: module_builder) (loc: location) (m: string list) =
end
let register () =
- begin
- Format.printf "[test-import] Registering 'foo'.@." ;
- Acsl_extension.register_module_importer "foo" loader ;
- end
+ Acsl_extension.register_module_importer ~plugin:"myplugin1" "foo" loader;
+ Acsl_extension.register_module_importer ~plugin:"myplugin1" "bar" loader;
+ Acsl_extension.register_module_importer ~plugin:"myplugin2" "foo" loader;
+ if Kernel.GeneralDebug.get () = 1 then
+ Acsl_extension.register_module_importer ~plugin:"myplugin1" "foo" loader
let () = Cmdline.run_after_extended_stage register
--
GitLab