diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll index 5aef82eb76078dc339d8181e66e6b00258daed77..5d83bbc63c40b026f08077b505cf31ccab06d6f3 100644 --- a/src/kernel_internals/parsing/clexer.mll +++ b/src/kernel_internals/parsing/clexer.mll @@ -573,7 +573,7 @@ rule initial = parse end else begin let start = Lexing.lexeme_start_p lexbuf in let source = Cil_datatype.Position.of_lexing_pos start in - Kernel.abort ~source "Use of \\ghost out of ghost code" + E.parse_error ~source "Use of \\ghost out of ghost code" end } diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 084eb5824356fed1965266ae9e5e5b895929c637..666053a2830b8b449ef19dc859732f997842f7bc 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -1471,7 +1471,7 @@ cvspec: if String.compare annot "\\ghost" = 0 then begin let start = Parsing.symbol_start_pos () in let source = Cil_datatype.Position.of_lexing_pos start in - Kernel.abort ~source "Use of \\ghost out of ghost code" + Errorloc.parse_error ~source "Use of \\ghost out of ghost code" end else SpecCV(CV_ATTRIBUTE_ANNOT annot), loc } diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle index c9a4f54903239d12c44e6f4483016d28e1eda919..11e0f79f7ac8199f0d10116325a2dfb06f0b267f 100644 --- a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle +++ b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle @@ -1,6 +1,14 @@ [kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing) -[kernel] tests/syntax/ghost_cv_parsing_errors.c:13: User Error: - Use of \ghost out of ghost code -[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors. - Add '-kernel-msg-key pp' for preprocessing command. +[kernel] tests/syntax/ghost_cv_parsing_errors.c:11: + Use of \ghost out of ghost code: + Location: between lines 11 and 13, before or at token: \ghost + 9 #ifdef IN_TYPE + 10 + + 11 struct S { + 12 int a ; + 13 } \ghost ; + + 14 + 15 #endif [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle index e5d6e9f1545603d3084395f99831a23d76d37721..79a1e05ec98cfb5e45d89f7936d79fcabc1dbd21 100644 --- a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle +++ b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle @@ -1,6 +1,11 @@ [kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing) -[kernel] tests/syntax/ghost_cv_parsing_errors.c:19: User Error: - Use of \ghost out of ghost code -[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors. - Add '-kernel-msg-key pp' for preprocessing command. +[kernel] tests/syntax/ghost_cv_parsing_errors.c:19: + Use of \ghost out of ghost code: + Location: line 19, between columns 0 and 4, before or at token: \ghost + 17 #ifdef IN_DECL + 18 + 19 int \ghost global ; + ^^^^^^^^^^^^^^^^^^^ + 20 + 21 #endif [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle index 2cb2aecf5c426c0fb746d2375780ee122af350d9..221217ee8deff4d92b722f17e10e341859edccb3 100644 --- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle +++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle @@ -1,6 +1,11 @@ [kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing) -[kernel] tests/syntax/ghost_cv_parsing_errors.c:25: User Error: - Use of \ghost out of ghost code -[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors. - Add '-kernel-msg-key pp' for preprocessing command. +[kernel] tests/syntax/ghost_cv_parsing_errors.c:25: + Use of \ghost out of ghost code: + Location: line 25, between columns 14 and 14 + 23 #ifdef IN_GHOST_ATTR + 24 + 25 int /*@ \ghost */ global ; + ^^^^^^^^^^^^^^^^^^^^^^^^^^ + 26 + 27 #endif [kernel] Frama-C aborted: invalid user input.