From f4f6909797f23cbc09cd05e3126fe9966a8decbc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 26 Feb 2024 10:20:58 +0100
Subject: [PATCH] [tests] new tests for location of parsing error

---
 tests/syntax/error_end_decl.i                      | 13 +++++++++++++
 tests/syntax/oracle/error_end_decl.res.oracle      |  0
 tests/syntax/oracle/static_assert_wrong.res.oracle |  9 +++++++++
 tests/syntax/static_assert_wrong.i                 |  8 ++++++++
 4 files changed, 30 insertions(+)
 create mode 100644 tests/syntax/error_end_decl.i
 create mode 100644 tests/syntax/oracle/error_end_decl.res.oracle
 create mode 100644 tests/syntax/oracle/static_assert_wrong.res.oracle
 create mode 100644 tests/syntax/static_assert_wrong.i

diff --git a/tests/syntax/error_end_decl.i b/tests/syntax/error_end_decl.i
new file mode 100644
index 00000000000..8fba5808d55
--- /dev/null
+++ b/tests/syntax/error_end_decl.i
@@ -0,0 +1,13 @@
+/* run.config
+EXIT: 1
+STDOPT:
+*/
+
+/*@ assigns *p \from \nothing; */
+void f(char *p)
+
+/*@
+  assigns \result \from \nothing;
+  ensures \result == 0;
+*/
+char g(char *p);
diff --git a/tests/syntax/oracle/error_end_decl.res.oracle b/tests/syntax/oracle/error_end_decl.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/syntax/oracle/static_assert_wrong.res.oracle b/tests/syntax/oracle/static_assert_wrong.res.oracle
new file mode 100644
index 00000000000..d2e83bab9e6
--- /dev/null
+++ b/tests/syntax/oracle/static_assert_wrong.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing static_assert_wrong.i (no preprocessing)
+[kernel] static_assert_wrong.i:8: 
+  syntax error:
+  Location: line 8, between columns 0 and 3, before or at token: int
+  6     _Static_assert(1,"assert succeeds")
+  7     
+  8     int x = 0;
+        ^^^
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/static_assert_wrong.i b/tests/syntax/static_assert_wrong.i
new file mode 100644
index 00000000000..fd27a5c70f7
--- /dev/null
+++ b/tests/syntax/static_assert_wrong.i
@@ -0,0 +1,8 @@
+/* run.config*
+   EXIT: 1
+   STDOPT:
+*/
+
+_Static_assert(1,"assert succeeds")
+
+int x = 0;
-- 
GitLab