From f7ef00a4f24b989fd5b7f23eade518d62a4d7e34 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Mar 2024 11:02:33 +0100
Subject: [PATCH] [kernel/logic] test for module syntax

---
 tests/spec/module.i                 | 8 ++++++++
 tests/spec/oracle/module.res.oracle | 5 +++++
 2 files changed, 13 insertions(+)
 create mode 100644 tests/spec/module.i
 create mode 100644 tests/spec/oracle/module.res.oracle

diff --git a/tests/spec/module.i b/tests/spec/module.i
new file mode 100644
index 0000000000..5198060dd0
--- /dev/null
+++ b/tests/spec/module.i
@@ -0,0 +1,8 @@
+/* run.config
+   EXIT: 1
+   OPT:
+ */
+
+/*@
+  logic integer next(integer x) = int::Int::add(x,1);
+ */
diff --git a/tests/spec/oracle/module.res.oracle b/tests/spec/oracle/module.res.oracle
new file mode 100644
index 0000000000..809701e2a7
--- /dev/null
+++ b/tests/spec/oracle/module.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing module.i (no preprocessing)
+[kernel:annot-error] module.i:7: Warning: 
+  lexical error, unexpected long identifier
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] Frama-C aborted: invalid user input.
-- 
GitLab