diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll index 71d54b7ee3449b04cebdab892e97bdc67ada3112..5745e3cc4ab7dedb8ed30f51c166cdbf558ab511 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 0000000000000000000000000000000000000000..b1068a026017e0292da90cf30ffe622ec3e41727 --- /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 0000000000000000000000000000000000000000..ce1df7885b2187e0dcfd219185697ce0580462c5 --- /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