From 69f759665b9b861c26cf95ba6be9e5b152b33b3f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 13 Jul 2021 19:27:36 +0200
Subject: [PATCH] [lexer] Proper error message in case of unfinished one-line
comment
---
src/kernel_internals/parsing/clexer.mll | 1 +
.../unfinished-oneline-acsl-comment.res.oracle | 12 ++++++++++++
tests/spec/unfinished-oneline-acsl-comment.i | 6 ++++++
3 files changed, 19 insertions(+)
create mode 100644 tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle
create mode 100644 tests/spec/unfinished-oneline-acsl-comment.i
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 71d54b7ee34..5745e3cc4ab 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -924,6 +924,7 @@ and annot_one_line = parse
| "" { annot_one_line_logic lexbuf }
and annot_one_line_logic = parse
| '\n' { make_annot ~one_line:true initial lexbuf (Buffer.contents buf) }
+ | eof { E.parse_error "Invalid C file: should end with a newline" }
| _ as c { Buffer.add_char buf c; annot_one_line_logic lexbuf }
{
diff --git a/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle b/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle
new file mode 100644
index 00000000000..b1068a02601
--- /dev/null
+++ b/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/spec/unfinished-oneline-acsl-comment.i (no preprocessing)
+[kernel] :0:
+ Invalid C file: should end with a newline:
+ Location: between <unknown> and 6:7, before or at token:
+
+ 1 /* run.config
+ 2 EXIT: 1
+ 3 STDOPT:
+ 4 */
+ 5 // If you edit this file, make sure it ends WITHOUT a newline
+ 6 //@ bad
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/unfinished-oneline-acsl-comment.i b/tests/spec/unfinished-oneline-acsl-comment.i
new file mode 100644
index 00000000000..ce1df7885b2
--- /dev/null
+++ b/tests/spec/unfinished-oneline-acsl-comment.i
@@ -0,0 +1,6 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+ */
+// If you edit this file, make sure it ends WITHOUT a newline
+//@ bad
\ No newline at end of file
--
GitLab