[lexer] Proper error message in case of unfinished one-line comment

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 }
 
 {

tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle

+[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.

tests/spec/unfinished-oneline-acsl-comment.i

+/* run.config
+   EXIT: 1
+   STDOPT:
+ */
+// If you edit this file, make sure it ends WITHOUT a newline
+//@ bad
\ No newline at end of file