diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 40341eef3217c41faa876a7a04c7bc8398c8e918..84b23d1063a300c4b1ccfcdd4af38fc37bcd89fd 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -52,6 +52,12 @@ module H = Hashtbl
module E = Errorloc
let currentLoc () = E.currentLoc ()
+let parse_error lexbuf msg =
+ let loc =
+ Cil_datatype.Location.of_lexing_loc
+ (lexbuf.Lexing.lex_start_p,lexbuf.Lexing.lex_curr_p)
+ in
+ E.parse_error ~loc msg
(* Convert char into Int64 *)
let int64_of_char c = Int64.of_int (Char.code c)
@@ -273,7 +279,7 @@ let finish () =
(*** escape character management ***)
-let scan_escape = function
+let scan_escape lexbuf = function
| 'n' -> int64_of_char '\n'
| 'r' -> int64_of_char '\r'
| 't' -> int64_of_char '\t'
@@ -290,7 +296,7 @@ let scan_escape = function
| '[' -> int64_of_char '['
| '%' -> int64_of_char '%'
| '\\' -> int64_of_char '\\'
- | other -> E.parse_error "Unrecognized escape sequence: \\%c" other
+ | other -> parse_error lexbuf "Unrecognized escape sequence: \\%c" other
let scan_hex_escape str =
let radix = Int64.of_int 16 in
@@ -324,7 +330,7 @@ let lex_oct_escape remainder lexbuf =
let lex_simple_escape remainder lexbuf =
let lexchar = Lexing.lexeme_char lexbuf 1 in
- let prefix = scan_escape lexchar in
+ let prefix = scan_escape lexbuf lexchar in
prefix :: remainder lexbuf
let lex_unescaped remainder lexbuf =
@@ -415,11 +421,6 @@ let make_annot ~one_line default lexbuf s =
| Logic_ptree.Aloop_annot (loc,a) -> LOOP_ANNOT (a,loc)
| Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc)
-let parse_error lexbuf msg =
- let loc = lexbuf.Lexing.lex_curr_p in
- let source = Cil_datatype.Position.of_lexing_pos loc in
- E.parse_error ~source msg
-
(* Initialize the pointer in Errormsg *)
let () =
Lexerhack.add_type := add_type ;
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 833e0631f2cf8ac3946248d27c4fbfa30dd3aef8..3a7000e478ed5fd0f64cea7570b811bfef34eac6 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -1577,7 +1577,6 @@ cvspec:
{
let annot, loc = $1 in
if String.compare annot "\\ghost" = 0 then begin
- let loc = Cil_datatype.Location.of_lexing_loc $loc in
Errorloc.parse_error ~loc "Use of \\ghost out of ghost code"
end else
SpecCV(CV_ATTRIBUTE_ANNOT annot), loc
diff --git a/tests/syntax/oracle/empty_base.0.res.oracle b/tests/syntax/oracle/empty_base.0.res.oracle
index e0b917dec36cf5e98a9ca3de169f9f4359d6f917..989cc122c482b696749c24b9c8b580a7edafcc1f 100644
--- a/tests/syntax/oracle/empty_base.0.res.oracle
+++ b/tests/syntax/oracle/empty_base.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing empty_base.c (with preprocessing)
[kernel] empty_base.c:63: User Error:
variable `c' has initializer but incomplete type
-[kernel] empty_base.c:67: Warning: Too many initializers for structure
+[kernel] empty_base.c:70: Warning: Too many initializers for structure
[kernel] empty_base.c:81: User Error:
non-final field `f1' declared with a type containing a flexible array member.
[kernel] User Error: stopping on file "empty_base.c" that has errors. Add '-kernel-msg-key pp'
diff --git a/tests/syntax/oracle/empty_base.1.res.oracle b/tests/syntax/oracle/empty_base.1.res.oracle
index bba69f8432c7a4c311b70f979773601645d4e353..b4a399dcf365d8ce1b017d51ac57d98c3821e4f4 100644
--- a/tests/syntax/oracle/empty_base.1.res.oracle
+++ b/tests/syntax/oracle/empty_base.1.res.oracle
@@ -14,7 +14,7 @@
48 struct empty empty_array_of_empty[0];
49 struct empty array_of_empty[1];
50 struct empty many_empty[3] = {{}};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^
51
52 comp array_of_comp[1] = {{.a = 17, .b = 45, .e = {}}};
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.1.res.oracle b/tests/syntax/oracle/generic.1.res.oracle
index 68c2dc2c614f19cbe6c1a83b91f8c2693b0853cb..c8f6605be6dcb690f616c3dd9bcdf7fc7226ea19 100644
--- a/tests/syntax/oracle/generic.1.res.oracle
+++ b/tests/syntax/oracle/generic.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel] generic.c:36:
_Generic requires at least one generic association:
- Location: line 36, between columns 25 and 26, before or at token: ;
+ Location: line 36, between columns 10 and 25, before or at token: ;
34 int main() {
35 #ifdef NONE
36 int a = _Generic("abc");
- ^
+ ^^^^^^^^^^^^^^^
37 #endif
38 #ifdef TOO_MANY_DEFAULTS
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.8.res.oracle b/tests/syntax/oracle/generic.8.res.oracle
index d77e640dffce97e0f22e3248a21e6bbf9404f726..fe35717281298c85c4a8ef02888473d4a3b90dce 100644
--- a/tests/syntax/oracle/generic.8.res.oracle
+++ b/tests/syntax/oracle/generic.8.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel] generic.c:62:
syntax error:
- Location: line 62, between columns 27 and 30, before or at token: int
+ Location: line 62, column 27, before or at token: int
60 #endif
61 #ifdef FUNCTION_TYPE
62 int a = _Generic(1, void(int): 1);
- ^^^
+ ^
63 #endif
64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
[kernel] Frama-C aborted: invalid user input.
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 556ea0b473fac93292764b80b5e1b73afd3b187a..49cee6b2fe416da7b33a5720a1990948067c181d 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
[kernel] ghost_cv_parsing_errors.c:14:
Use of \ghost out of ghost code:
- Location: line 14, between columns 0 and 8, before or at token: \ghost
+ Location: line 14, between columns 2 and 8, before or at token: \ghost
12 struct S {
13 int a ;
14 } \ghost ;
- ^^^^^^^^
+ ^^^^^^
15
16 #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 1060fb309d1c43c99c47d33d4eebefb6b52cdc77..0926c5ae2e4187081e7419b260018facdbd518c7 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
[kernel] ghost_cv_parsing_errors.c:20:
Use of \ghost out of ghost code:
- Location: line 20, between columns 0 and 10, before or at token: \ghost
+ Location: line 20, between columns 4 and 10, before or at token: \ghost
18 #ifdef IN_DECL
19
20 int \ghost global ;
- ^^^^^^^^^^
+ ^^^^^^
21
22 #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 743cdf3cdb3c454aae8cd5bd9ef9bee2ec6d96b1..23eb9fb13e2f2b46c7f11cc6eceed5cdcec73e4b 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
[kernel] ghost_cv_parsing_errors.c:26:
Use of \ghost out of ghost code:
- Location: line 26, column 14, before or at token: global
+ Location: line 26, between columns 8 and 14, before or at token: global
24 #ifdef IN_GHOST_ATTR
25
26 int /*@ \ghost */ global ;
- ^
+ ^^^^^^
27
28 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_else_bad.2.res.oracle b/tests/syntax/oracle/ghost_else_bad.2.res.oracle
index 5bf78d1d17d803aff751627e061c065d913c110c..c72e9cf52cd938bacdb4e12ebebc45366787f0b6 100644
--- a/tests/syntax/oracle/ghost_else_bad.2.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.2.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_else_bad.c (with preprocessing)
[kernel] ghost_else_bad.c:49:
syntax error:
- Location: line 49, between columns 5 and 9, before or at token: else
+ Location: line 49, between columns 0 and 5, before or at token: else
47 } /*@ ghost
48 //@ ensures \true ;
49 else {
- ^^^^
+ ^^^^^
50 y++ ;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle b/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
index 2b50bccd39dedcfb69009075669398cfe856ba20..031c56441d08521ae27a25634ff32eb4c0791a1a 100644
--- a/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
@@ -1,13 +1,12 @@
[kernel] Parsing ghost_else_bad_oneline.i (no preprocessing)
[kernel] ghost_else_bad_oneline.i:8:
syntax error:
- Location: between lines 8 and 9, before or at token:
+ Location: line 8, column 18, before or at token:
6 if (x) {
7 x++;
-
8 } //@ ghost else
+ ^
9 y++;
-
10 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle
index f78f3f7ccd20e4a34d9a03388a0fb55e9db7e090..77dc1648f28a1fae531786aad864e14528d49d60 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle
@@ -1,13 +1,11 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
-[kernel] ghost_multiline_annot.c:48:
+[kernel] ghost_multiline_annot.c:49:
This kind of annotation is valid only inside ghost code:
- Location: between lines 48 and 49, before or at token: /@
- 46 #ifdef P2
+ Location: line 49, between columns 2 and 4, before or at token: /@
47 int main()
-
48 {
49 /@ assert 2 == 2; @/
-
+ ^^
50 return 0;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
index 5abb405a7688c062f621226200b256b1da5916d1..2a1317e6562358993c37fbec5f462d91126a7f27 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
[kernel] ghost_multiline_annot.c:57:
Invalid symbol:
- Location: line 57, between columns 17 and 20, before or at token: @
+ Location: line 57, between columns 19 and 20, before or at token: @
55 int main()
56 {
57 assert (2 == 2); @/
- ^^^
+ ^
58 return 0;
59 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.11.res.oracle b/tests/syntax/oracle/ghost_parameters.11.res.oracle
index 481f6d945559a12cd7ea6b6d2b3b44b90224a99c..c649da62073f64858ab47dcccc22ee39abbe6a5a 100644
--- a/tests/syntax/oracle/ghost_parameters.11.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.11.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing ghost_parameters.c (with preprocessing)
[kernel] ghost_parameters.c:195:
syntax error:
- Location: line 195, between columns 36 and 37, before or at token: )
+ Location: line 195, column 36, before or at token: )
193 #ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
194
195 void function_void(void) /*@ ghost () */ {
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
index e6dd04f33e9b7840c7f4a4d8d884fa362b6daeb6..72045be30e748f3a23d52fa5bf88c2f8140ef868 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
@@ -5,7 +5,7 @@
31
32 /*@ ghost void function(void){ } */
33 void function(void) ;
- ^^^^
+ ^^^^^^^^
34
35 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
index d75f41a1ba1dad33bb8bca4163eab7f693a6d10e..d429e28777b75d7f9d2699584783bc69529627c4 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
@@ -5,7 +5,7 @@
42
43 void function(void){ }
44 /*@ ghost void function(void) ; */
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
45
46 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/init_bts1352.res.oracle b/tests/syntax/oracle/init_bts1352.res.oracle
index f38741556ecfae1c1e706ec18f985659d0687909..e6d8d227b4510643f819c200d7cd3a0fc3d793bc 100644
--- a/tests/syntax/oracle/init_bts1352.res.oracle
+++ b/tests/syntax/oracle/init_bts1352.res.oracle
@@ -4,6 +4,6 @@
6
7 int main(void) {
8 int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
9 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle b/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
index 507b75f850f52a8e8ca5a4fbcb70fed6ce83f536..1d7458f98dd1567775551f62b4177d14d6903e44 100644
--- a/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
+++ b/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
@@ -5,6 +5,6 @@
12
13 void f(FILE *file) {
14 (*(T*)&B) = 0; // error: implicit cast: cannot cast from int to T
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
15 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/line_number.res.oracle b/tests/syntax/oracle/line_number.res.oracle
index 8f92b8bb7cdd6e1ddb1e9565c894fd9015e468e1..dba6ed32a4142f9562c93d8de3bde49c7758bf27 100644
--- a/tests/syntax/oracle/line_number.res.oracle
+++ b/tests/syntax/oracle/line_number.res.oracle
@@ -5,6 +5,6 @@
4 */
5
6 //@ assert \result == 0;
- ^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
7 extern int p(void void);
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/localisation_error.res.oracle b/tests/syntax/oracle/localisation_error.res.oracle
index 3b608a622ead61895bc3c8665719a3cdaef13f08..a99a0894ae2dd6de7e3610fbfa264ba454971f9b 100644
--- a/tests/syntax/oracle/localisation_error.res.oracle
+++ b/tests/syntax/oracle/localisation_error.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing localisation_error.i (no preprocessing)
[kernel] localisation_error.i:7:
syntax error:
- Location: line 7, between columns 57 and 58, before or at token: /
+ Location: line 7, column 57, before or at token: /
5 int main() {
6 int b = 0;
7 //@ ghost int a = 2; /*@ assert a == 3; */ /* test */ */
diff --git a/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle b/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
index 5c29aee6daded821f472bdf4600fe4657cc83294..a7eee9649423c175a124e16cbefcbbacc2ddb639 100644
--- a/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
+++ b/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
@@ -1,11 +1,13 @@
[kernel] Parsing spurious_brace_bts_1273.i (no preprocessing)
-[kernel] spurious_brace_bts_1273.i:8:
+[kernel] spurious_brace_bts_1273.i:7:
syntax error:
- Location: line 8, between columns 0 and 1, before or at token: }
+ Location: between lines 7 and 8, before or at token: }
+ 5
6 void foo() {
+
7 }
8 }
- ^
+
9
10 void main () {
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/syntactic_hook.res.oracle b/tests/syntax/oracle/syntactic_hook.res.oracle
index 36eadea81f3b5b6bd52fb3eb0797126e9bfe2d4f..19d5998e0ad1e79fd5a7fa4e388476c31f59be9d 100644
--- a/tests/syntax/oracle/syntactic_hook.res.oracle
+++ b/tests/syntax/oracle/syntactic_hook.res.oracle
@@ -43,5 +43,5 @@
28 }
29
30 int f(int); //error: conflicting decls
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
index 9a3b3fba23393d8e1c25b9162d0e30c244bddb98..6dfc1df3a047e00c0284e137f3bfe697da90b3af 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing typedef_namespace_bts1500.c (with preprocessing)
[kernel] typedef_namespace_bts1500.c:24:
syntax error:
- Location: line 24, between columns 8 and 9, before or at token: y
+ Location: line 24, between columns 7 and 8, before or at token: y
22 // error: digit is now a variable
23 #ifdef HIDING_TYPEDEF
24 digit y = 5;
- ^
+ ^
25 #endif
26 return x + digit+A;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong_label.res.oracle b/tests/syntax/oracle/wrong_label.res.oracle
index 09dedc1be826a7b75581602889a0d57cb6d51155..3103fda144a35c1adeaed71ffc9a2c418ebcfa60 100644
--- a/tests/syntax/oracle/wrong_label.res.oracle
+++ b/tests/syntax/oracle/wrong_label.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing wrong_label.i (no preprocessing)
[kernel] wrong_label.i:11:
syntax error:
- Location: line 11, between columns 8 and 9, before or at token: }
+ Location: line 11, column 8, before or at token: }
9
10 void main() {
11 {_LOR:} // KO: labels can't be at the end of a block.