From b0bddd21dd7446ac00927b9a84bcf638cadd83d1 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 19 Mar 2020 08:40:51 +0100
Subject: [PATCH] [ghost] Changes parsing-error for \ghost qualifier
---
src/kernel_internals/parsing/clexer.mll | 2 +-
src/kernel_internals/parsing/cparser.mly | 2 +-
.../oracle/ghost_cv_parsing_errors.0.res.oracle | 16 ++++++++++++----
.../oracle/ghost_cv_parsing_errors.1.res.oracle | 13 +++++++++----
.../oracle/ghost_cv_parsing_errors.2.res.oracle | 13 +++++++++----
5 files changed, 32 insertions(+), 14 deletions(-)
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 5aef82eb760..5d83bbc63c4 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 084eb582435..666053a2830 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 c9a4f549032..11e0f79f7ac 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 e5d6e9f1545..79a1e05ec98 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 2cb2aecf5c4..221217ee8de 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.
--
GitLab