diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml
index c1a5effb6b7484adcca17c7600734013808be513..31b21bccd37d9d703941c1526e157e10743e0f27 100644
--- a/src/kernel_internals/parsing/errorloc.ml
+++ b/src/kernel_internals/parsing/errorloc.ml
@@ -142,15 +142,19 @@ let setCurrentFile n =
plus up to [ctx] lines before and after [pos.pos_lnum] (if they exist),
similar to 'grep -C<ctx>'. The first line is numbered 1.
Most exceptions are silently caught and printing is stopped if they occur. *)
-let pp_context_from_file ?(ctx=2) ?start_line ?(start_char=1) fmt pos =
+let pp_context_from_file ?(ctx=2) ?start_pos fmt pos =
try
let in_ch = open_in (pos.Filepath.pos_path :> string) in
try
begin
- let first_error_line, last_error_line =
- match start_line with
- | None -> pos.Filepath.pos_lnum, pos.Filepath.pos_lnum
- | Some l -> min l pos.Filepath.pos_lnum, max l pos.Filepath.pos_lnum
+ let open Filepath in
+ let first_error_line, start_char, last_error_line =
+ match start_pos with
+ | None -> pos.pos_lnum, 1, pos.pos_lnum
+ | Some s ->
+ min s.pos_lnum pos.pos_lnum,
+ (s.pos_cnum - s.pos_bol + 1),
+ max s.pos_lnum pos.pos_lnum
in
(* The difference between the first and last error lines can be very
large; in this case, we print only the first and last [error_ctx]
@@ -292,11 +296,7 @@ let parse_error ?source msg =
pp_location (start_pos, last_pos)
pretty_token (Lexing.lexeme current.lexbuf);
Format.fprintf fmt "%a@."
- (pp_context_from_file
- ~start_line:start_pos.Filepath.pos_lnum
- ~ctx:2
- ~start_char:(start_pos.pos_cnum - start_pos.pos_bol + 1))
- last_pos);
+ (pp_context_from_file ~start_pos ~ctx:2) last_pos);
raise (Log.AbortError "kernel"))
msg
diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli
index 3d2163ab12926acc0a0a5b1e10530c254e02bff8..e067ebd1d200aa1c1c0dae82c421c409f7e930bc 100644
--- a/src/kernel_internals/parsing/errorloc.mli
+++ b/src/kernel_internals/parsing/errorloc.mli
@@ -68,14 +68,15 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and
(** prints the line identified by the position, together with [ctx] lines
of context before and after. [ctx] defaults to 2.
- If [start_line] is specified, then all lines between [start_line] and
- [pos.pos_lnum] are considered part of the error.
- If [start_line] and [pos.pos_lnum] are identical (or [start_line] is None),
- the portion of the line between [start_char] (defaults to 1) and
- the character position indicated by [pos] is underlined with [^].
+ If [start_pos] is specified, then all positions between [start_pos] and
+ [pos] are considered part of the error. If this expands to multiple
+ lines, those lines will be separated from context by blank lines.
+ Otherwise, the portion of the line that is between the two positions
+ will be underlined with [^]
+ @before Frama-C+dev: [start_pos] was named [start_line] (and was an [int]).
*)
val pp_context_from_file:
- ?ctx:int -> ?start_line:int -> ?start_char:int ->
+ ?ctx:int -> ?start_pos:Filepath.position ->
Format.formatter -> Filepath.position -> unit
(** prints a readable description of a location
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index d98f976c73898a1ec6b4cd9e749e7dc7405908c2..4e13f8455dde1898f6b597576558104751360eca 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -128,11 +128,10 @@ let typeForInsertedVar: (Cil_types.typ -> Cil_types.typ) ref = ref (fun t -> t)
let cabs_exp loc node = { expr_loc = loc; expr_node = node }
let abort_context msg =
- let (p1,p2) = Cil.CurrentLoc.get() in
+ let start_pos,end_pos = Cil.CurrentLoc.get() in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file
- ~start_line:p1.pos_lnum ~start_char:(p1.pos_cnum -p1.pos_bol) fmt p2
+ Errorloc.pp_context_from_file ~start_pos fmt end_pos
in
Kernel.abort ~current:true ~append msg
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index 52cfe20c61e49d31fef4776a1cf8dc8f32c6e3bc..03706bd02db08d147cfbd6c353e5672083097bec 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -25,16 +25,17 @@
open Lexing
-let current_loc lex = Cil_datatype.Position.of_lexing_pos (lexeme_start_p lex)
-
let abort_current lex fmt =
- let source = current_loc lex in
- let start_line = source.Filepath.pos_lnum in
- let start_char = source.pos_cnum - source.pos_bol in
+ let start_pos =
+ Cil_datatype.Position.of_lexing_pos (lexeme_start_p lex)
+ in
+ let end_pos =
+ Cil_datatype.Position.of_lexing_pos (lexeme_end_p lex)
+ in
let fmt = "before or at token %s@\n%a@\n" ^^ fmt in
- Aorai_option.abort ~source fmt
+ Aorai_option.abort fmt
(Lexing.lexeme lex)
- (Errorloc.pp_context_from_file ~start_line ~start_char ~ctx:2) source
+ (Errorloc.pp_context_from_file ~start_pos ~ctx:2) end_pos
let unknown_token lex =
abort_current lex
diff --git a/src/plugins/aorai/utils_parser.mli b/src/plugins/aorai/utils_parser.mli
index 94495b62110040746c4b95118a696feec6cc7c6d..65d6018cc86c8d969b9696ef6d211d79e07d264a 100644
--- a/src/plugins/aorai/utils_parser.mli
+++ b/src/plugins/aorai/utils_parser.mli
@@ -25,10 +25,6 @@
(** utilities for parsing automaton's formulas *)
-(** returns the position corresponding to the
- current character in the lexbuf. *)
-val current_loc: Lexing.lexbuf -> Cil_datatype.Position.t
-
(** aborts the execution using current lexbuf position as source. *)
val abort_current:
Lexing.lexbuf -> ('a, Format.formatter, unit, 'b) format4 -> 'a
diff --git a/tests/misc/oracle/bts0451.res.oracle b/tests/misc/oracle/bts0451.res.oracle
index 909322412f84fc085ec941eaeb91d24b853f3097..0fbb9f6d610f59aa42578578fc8b9fd172bc3c66 100644
--- a/tests/misc/oracle/bts0451.res.oracle
+++ b/tests/misc/oracle/bts0451.res.oracle
@@ -4,7 +4,7 @@
25 /* should abort with an error at type-checking */
26 int main (void) {
27 break;
- ^^^^^^^^
+ ^^^^^^
28 return 0;
29 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/localisation_error.i b/tests/syntax/localisation_error.i
new file mode 100644
index 0000000000000000000000000000000000000000..9ba065a77bc6e88452caada570660307c9a4b49d
--- /dev/null
+++ b/tests/syntax/localisation_error.i
@@ -0,0 +1,4 @@
+int main() {
+ int b = 0;
+ //@ ghost int a = 2; /*@ assert a == 3; */ /* test */ */
+}
diff --git a/tests/syntax/oracle/arg_type.res.oracle b/tests/syntax/oracle/arg_type.res.oracle
index 256d77be54eea88d5de89856edfa865ae4cd8abf..e38a0c4a8dbc72717d5f9bc66287becec04d567d 100644
--- a/tests/syntax/oracle/arg_type.res.oracle
+++ b/tests/syntax/oracle/arg_type.res.oracle
@@ -7,5 +7,5 @@
13 int g(int);
14
15 int g(short x) { return x; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/binary_op.0.res.oracle b/tests/syntax/oracle/binary_op.0.res.oracle
index 60dc2afc775623a14bdbf16138e62b32b11d1e61..ba9b4df4645c004647be9328520a4ac831ecd04a 100644
--- a/tests/syntax/oracle/binary_op.0.res.oracle
+++ b/tests/syntax/oracle/binary_op.0.res.oracle
@@ -4,7 +4,7 @@
9
10 #ifdef BITWISE
11 int v(void) { return 0 & v; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^
12 #endif
13
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/binary_op.1.res.oracle b/tests/syntax/oracle/binary_op.1.res.oracle
index b896f4027b9e1e78d89cc8d7ee7d295179e244cb..3c36f99b1ba2ca134d9bf826a1cfb7919a94580a 100644
--- a/tests/syntax/oracle/binary_op.1.res.oracle
+++ b/tests/syntax/oracle/binary_op.1.res.oracle
@@ -4,7 +4,7 @@
13
14 #ifdef MULT
15 int w(void) { return 0 * w; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^
16 #endif
17
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.0.res.oracle b/tests/syntax/oracle/cert_msc_38.0.res.oracle
index 35b7a148eb975f2de2aba45c97a7c741df1d3ab6..f6a1827a00ee1aa706ca699b14dfed85be6f92fc 100644
--- a/tests/syntax/oracle/cert_msc_38.0.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.0.res.oracle
@@ -6,7 +6,7 @@
24 void func(int e) {
25 // error: assert must be a macro, not a function
26 execute_handler(&(assert), e < 0);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
27 }
28
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.3.res.oracle b/tests/syntax/oracle/cert_msc_38.3.res.oracle
index 218315e21b14ed0d0a190d1042df3801383989b1..2e259dde2946d6569e10c5a4cc95a858c1737dbe 100644
--- a/tests/syntax/oracle/cert_msc_38.3.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.3.res.oracle
@@ -6,7 +6,7 @@
41 // error: can't suppress va_* macros
42 #ifdef TEST_VASTART
43 void *(*test1)() = &(va_start);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
44 #endif
45
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.4.res.oracle b/tests/syntax/oracle/cert_msc_38.4.res.oracle
index 0fc570c7b670da969e4e103274aa5a031fa77d53..0ede081258a48c2c8b7b39f35ea4dbf7c520b3c9 100644
--- a/tests/syntax/oracle/cert_msc_38.4.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.4.res.oracle
@@ -6,7 +6,7 @@
45
46 #ifdef TEST_VACOPY
47 void (*test2)() = &(va_copy);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^
48 #endif
49
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.5.res.oracle b/tests/syntax/oracle/cert_msc_38.5.res.oracle
index 880f1b230eb0b5c44e5c6b09bc3c209c356842c9..9d7c6211083229cedc0417493187e8962410c61c 100644
--- a/tests/syntax/oracle/cert_msc_38.5.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.5.res.oracle
@@ -6,7 +6,7 @@
49
50 #ifdef TEST_VAARG
51 void* (*test3)() = &(va_arg);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
52 #endif
53
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.6.res.oracle b/tests/syntax/oracle/cert_msc_38.6.res.oracle
index 507ff0d508144acc5759a7f2a9199a02ecaf923a..7ae19b28c59175c9f7070afea5a74d61cb984a01 100644
--- a/tests/syntax/oracle/cert_msc_38.6.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.6.res.oracle
@@ -6,7 +6,7 @@
53
54 #ifdef TEST_VAEND
55 void (*test4)() = &(va_end);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
56 #endif
57
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.1.res.oracle b/tests/syntax/oracle/const-assignments.1.res.oracle
index fa6f9af638d0448cc55fd8c5a71071d0c5d2b33d..36093e3713d667b3a4b4c14a4afbdb667e6ffcab 100644
--- a/tests/syntax/oracle/const-assignments.1.res.oracle
+++ b/tests/syntax/oracle/const-assignments.1.res.oracle
@@ -4,7 +4,7 @@
20 #ifdef T0
21 void f() {
22 x = 42;
- ^^^^^^^^^
+ ^^^^^^
23 }
24 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.2.res.oracle b/tests/syntax/oracle/const-assignments.2.res.oracle
index 2dc9215a35ac450654652550a7134ac578f0d973..02f6615a1ee9edc00bfd905532236f7cd552ff30 100644
--- a/tests/syntax/oracle/const-assignments.2.res.oracle
+++ b/tests/syntax/oracle/const-assignments.2.res.oracle
@@ -4,7 +4,7 @@
26 #ifdef T1
27 void f() {
28 x++;
- ^^^^^^
+ ^^^
29 }
30 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.3.res.oracle b/tests/syntax/oracle/const-assignments.3.res.oracle
index 23e5bce2386bd9bb6e8994cb30b9b89d71e63abf..d2d7a5d27abb6ffa65c46316ea62d0cd041fce66 100644
--- a/tests/syntax/oracle/const-assignments.3.res.oracle
+++ b/tests/syntax/oracle/const-assignments.3.res.oracle
@@ -4,7 +4,7 @@
32 #ifdef T2
33 void f() {
34 --x;
- ^^^^^^
+ ^^^
35 }
36 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.4.res.oracle b/tests/syntax/oracle/const-assignments.4.res.oracle
index e1fc81de7638961470872331b6a7e2ace1f35cef..f773542dfc5f2fbc140fbeee5c59bb82fa9b2994 100644
--- a/tests/syntax/oracle/const-assignments.4.res.oracle
+++ b/tests/syntax/oracle/const-assignments.4.res.oracle
@@ -4,7 +4,7 @@
38 #ifdef T3
39 void f() {
40 x += 3;
- ^^^^^^^^^
+ ^^^^^^
41 }
42 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.5.res.oracle b/tests/syntax/oracle/const-assignments.5.res.oracle
index 6149ca6c14a7ef7f6b9b4cb653bace5472af8f22..1bc8881f49e26ef1b0188b643d9189325442879c 100644
--- a/tests/syntax/oracle/const-assignments.5.res.oracle
+++ b/tests/syntax/oracle/const-assignments.5.res.oracle
@@ -4,7 +4,7 @@
45 void f() {
46 const int x = 2;
47 x *= 2;
- ^^^^^^^^^
+ ^^^^^^
48 }
49 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.6.res.oracle b/tests/syntax/oracle/const-assignments.6.res.oracle
index 75d299175cdf14a4c23369123383d94c83412930..0a47849f5a7f32f7bdd6893625e758209a9117c1 100644
--- a/tests/syntax/oracle/const-assignments.6.res.oracle
+++ b/tests/syntax/oracle/const-assignments.6.res.oracle
@@ -4,7 +4,7 @@
51 #ifdef T5
52 void f(const int* x) {
53 *x = 1;
- ^^^^^^^^^
+ ^^^^^^
54 }
55 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.9.res.oracle b/tests/syntax/oracle/const-assignments.9.res.oracle
index 1eac0647def6c209d2ae35d2137f82a76bcaecde..195a24229577ea26b31a04c6abd36f9f2b5c8eaa 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -4,7 +4,7 @@
119
120 void mutable_test_ko(const T* t) {
121 t->s.y = 32; // KO: although t->s could be modified, t->s.y is still const
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^
122 }
123
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle b/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle
index 0eca364b644783f7bffc52806e552a4d1ac4eb80..e5ce52792dbd7cc2bb7339417a402b1cc66eb3db 100644
--- a/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle
+++ b/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle
@@ -4,7 +4,7 @@
11 void (*p)(void) = &f ;
12 p = 1 ;
13 *p = 1 ;
- ^^^^^^^^^^
+ ^^^^^^
14 return 0 ;
15 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle b/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle
index 4bcdf11602646662df1553ed1c6d4b60bd297b50..e86474631363d992b654fe27948ccfac60aab5da 100644
--- a/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle
+++ b/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle
@@ -4,7 +4,7 @@
10 void (*p)(void) = &f ;
11 p = &f ;
12 *p = f ;
- ^^^^^^^^^^
+ ^^^^^^
13 return 0 ;
14 }
[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 07cb4e0900f35bf7656e01f4c4da47c996398609..68c2dc2c614f19cbe6c1a83b91f8c2693b0853cb 100644
--- a/tests/syntax/oracle/generic.1.res.oracle
+++ b/tests/syntax/oracle/generic.1.res.oracle
@@ -5,7 +5,7 @@
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.2.res.oracle b/tests/syntax/oracle/generic.2.res.oracle
index 97bc6f5808c4546a36098776a764a2b82d62c921..0edc5626dfd5157572f29d022cfbf997a14fba98 100644
--- a/tests/syntax/oracle/generic.2.res.oracle
+++ b/tests/syntax/oracle/generic.2.res.oracle
@@ -4,7 +4,7 @@
37 #endif
38 #ifdef TOO_MANY_DEFAULTS
39 int a = _Generic("abc", default: 1, default: 1);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
40 #endif
41 #ifdef TOO_MANY_COMPATIBLE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.3.res.oracle b/tests/syntax/oracle/generic.3.res.oracle
index e683c048013d632828688464c432aacd535c1d5c..af00e69e6f9a9db9d0453d3965d5af3f92f4deb1 100644
--- a/tests/syntax/oracle/generic.3.res.oracle
+++ b/tests/syntax/oracle/generic.3.res.oracle
@@ -5,7 +5,7 @@
41 #ifdef TOO_MANY_COMPATIBLE
42 // compatibility via typedef
43 int a = _Generic(42, my_uint: 1, unsigned int: 2);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
44 #endif
45 #ifdef TOO_MANY_COMPATIBLE2
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.4.res.oracle b/tests/syntax/oracle/generic.4.res.oracle
index f1c86c668f3b5d44078dd2fad20ee3189ae350f2..4dea267e9f5cf04b162f789e3847a6714d99c8a0 100644
--- a/tests/syntax/oracle/generic.4.res.oracle
+++ b/tests/syntax/oracle/generic.4.res.oracle
@@ -4,8 +4,11 @@
'void (*)()' and 'void (*)(void)'
45 #ifdef TOO_MANY_COMPATIBLE2
46 // compatibility modulo implicit arguments
+
47 int a = _Generic(0,
- ^^^^^^^^^^^^^^^^^^^^^
48 void (*)(): 0,
49 void (*)(void): 0);
+
+ 50 #endif
+ 51 #ifdef TOO_MANY_COMPATIBLE3
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.5.res.oracle b/tests/syntax/oracle/generic.5.res.oracle
index 47db165e125863871e8aa11d51329b948954a9ff..579b9dde7959145550bcea41382a8e721f40b21d 100644
--- a/tests/syntax/oracle/generic.5.res.oracle
+++ b/tests/syntax/oracle/generic.5.res.oracle
@@ -5,8 +5,11 @@
compatible types: void (*)(void), void (*)(int )
52 // implicit arguments compatible between first and second selector,
53 // but the selectors themselves are not compatible between them
+
54 int a = _Generic((void (*)()) 0,
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
55 void (*)(int): 0,
56 void (*)(void): 0);
+
+ 57 #endif
+ 58 #ifdef INCOMPLETE_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.6.res.oracle b/tests/syntax/oracle/generic.6.res.oracle
index 17b9dbce578c02ed0e29a79f18e4a5cc97fe53bb..fbfffc1be280933ec883e33e343a303d4541dd09 100644
--- a/tests/syntax/oracle/generic.6.res.oracle
+++ b/tests/syntax/oracle/generic.6.res.oracle
@@ -4,7 +4,7 @@
57 #endif
58 #ifdef INCOMPLETE_TYPE
59 int a = _Generic(42, void: 1, default: 2);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
60 #endif
61 #ifdef FUNCTION_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.7.res.oracle b/tests/syntax/oracle/generic.7.res.oracle
index b8635912296f2a8ab067e16ae5cd6c79e617740a..c232c3c417e6f8d49a53f25f9f116dc939d908b2 100644
--- a/tests/syntax/oracle/generic.7.res.oracle
+++ b/tests/syntax/oracle/generic.7.res.oracle
@@ -6,7 +6,7 @@
63 #endif
64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
65 int a = _Generic("abc", char const *: 0);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
66 #endif
67 int ok1 = _Generic("abc", char*: 0);
[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 d07d4fc7c3bf850b4f3952019549118ddfe091e9..d77e640dffce97e0f22e3248a21e6bbf9404f726 100644
--- a/tests/syntax/oracle/generic.8.res.oracle
+++ b/tests/syntax/oracle/generic.8.res.oracle
@@ -5,7 +5,7 @@
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 ccbca4666e4df299d560a288b948c2eb45309def..556ea0b473fac93292764b80b5e1b73afd3b187a 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
@@ -5,7 +5,7 @@
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 c6e7d874a8f04424b00edad07d8149bb2c69a414..1060fb309d1c43c99c47d33d4eebefb6b52cdc77 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
@@ -5,7 +5,7 @@
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_else_bad.0.res.oracle b/tests/syntax/oracle/ghost_else_bad.0.res.oracle
index 8c7597d919f243915e628427efbabb963df4021e..687b31dd0c0961e5eaa0d3866eabc41c09b62d8f 100644
--- a/tests/syntax/oracle/ghost_else_bad.0.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.0.res.oracle
@@ -4,7 +4,7 @@
18 } */
19
20 z = 42;
- ^^^^^^^^^
+ ^
21 }
22
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
index db076a7b7a6ec433049a8b98e4ce8eb693c051ac..fcab3b6edda80dcf54a7d33a081288b9362689f8 100644
--- a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
+++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
@@ -7,6 +7,6 @@
19 //@ ghost int c = 0;
20 // ill-formed: the instruction should be ghost as well
21 c++;
- ^^^^^^
+ ^
22 }
[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 ca5a43f04dd43c19ee1655ce25e9acc0626720ef..5abb405a7688c062f621226200b256b1da5916d1 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
@@ -5,7 +5,7 @@
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 27c61b15f1593906bbc287ba234bda4c02c8c342..481f6d945559a12cd7ea6b6d2b3b44b90224a99c 100644
--- a/tests/syntax/oracle/ghost_parameters.11.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.11.res.oracle
@@ -5,7 +5,7 @@
193 #ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
194
195 void function_void(void) /*@ ghost () */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
196
197 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
index 91706e15eaf26f9bedcea422d359921b82289b31..9b4dd9a90766818a45943c9ee2e9e289d1bc80e5 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
@@ -5,7 +5,7 @@
9
10 void function(void) ;
11 /*@ ghost void function(void){ } */
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
12
13 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
index 366eb65da8bebad673e81287f1547ce7ba696a8c..9c6cce1bd60612b82c08bcbb27e39af7a9581feb 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
@@ -5,7 +5,7 @@
20
21 /*@ ghost void function(void) ; */
22 void function(void){ }
- ^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
23
24 void user(void){
[kernel] Frama-C aborted: invalid user input.
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 35cfc826665ee35836dba7b90ce92b099648f190..e6dd04f33e9b7840c7f4a4d8d884fa362b6daeb6 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/localisation_error.res.oracle b/tests/syntax/oracle/localisation_error.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/syntax/oracle/lvalvoid.res.oracle b/tests/syntax/oracle/lvalvoid.res.oracle
index a43dffc8a880f058bfef52ebfded61cdad2cde23..bca0bd162992eb724b4d064e8082d926153db988 100644
--- a/tests/syntax/oracle/lvalvoid.res.oracle
+++ b/tests/syntax/oracle/lvalvoid.res.oracle
@@ -5,7 +5,7 @@
6 char* d=dst; char* s=src;
7 for (int i=0;i<n;i++)
8 d[i]=(char)(src[i]);
- ^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
9 return dst;
10 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/no_prototype.res.oracle b/tests/syntax/oracle/no_prototype.res.oracle
index c3a946c73e7cff7cd41935da87661bed4453c4c2..5cebe4f9f28a2c1a8b524a6f4d57087d5e9ce37c 100644
--- a/tests/syntax/oracle/no_prototype.res.oracle
+++ b/tests/syntax/oracle/no_prototype.res.oracle
@@ -9,7 +9,7 @@
9 foo();
10 }
11 void foo(int a) {
- ^^^^^^^^^^^^^^^^^
+ ^^^
12 int i = a ;
13 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
index 76603c68330d472624936e438e76176d33c1e163..8bf3f8034fb35482c554e9fce89ad7e732402528 100644
--- a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
+++ b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
@@ -9,7 +9,7 @@
17 }
18
19 int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
20 x = 17;
21 y=18;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
index 177b11f83f9963da63cc7a8b11fde507a1181387..1e4b063503a8d8763cea27368f2b61984d53617f 100644
--- a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
+++ b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
@@ -8,7 +8,7 @@
17 }
18
19 int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
20 x = 17;
21 y=18;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/type_branch_bts_1081.res.oracle b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
index 279e77e82b0a80efa541243786ebfbbf0a8f6e85..ea64e936b23e0310ebda4a4b2c078f8f30ee68f5 100644
--- a/tests/syntax/oracle/type_branch_bts_1081.res.oracle
+++ b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
@@ -4,7 +4,7 @@
8 foo ? (void)x : (signed char)y;
9 // accepted (we drop the expressions, don't care about their types)
10 int z = foo ? (void)x: (signed char)y; // rejected
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
11 return 0;
12 }
[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 382925a17d83920679a858652248efddf67a7fcf..9a3b3fba23393d8e1c25b9162d0e30c244bddb98 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
@@ -5,7 +5,7 @@
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/very_large_integers.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
index e74ad25634d44e2274a374ae907cbca71e904c37..dfa0361fdd0d0d4d5c61012271356b53d0c9e311 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -9,7 +9,7 @@
100 #ifdef ARRAY_INIT1
101 // Previously caused Invalid_argument(Array.make)
102 int a1[] = {[72057594037927936] = 0};
- ^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^
103 #endif
104
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index 3ded691db128b079cba777fce10a9415a15903f9..7cbdaf67c3bf4023f8a9718c4fdf3ad4a994aee4 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -10,7 +10,7 @@
112 // Previously caused Out of memory
113 struct st s = {
114 {{[7205759403792793 ... 7205759403792793] = 0}}
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
115 };
116 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
index b39f7c8df96db714552373dbfb3e1964cff2bd78..c50d81a831f04612f363830022c80e0b0cc7e6b8 100644
--- a/tests/syntax/oracle/very_large_integers.15.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -9,7 +9,7 @@
117
118 #ifdef ARRAY_INIT3
119 int ai3[] = {0xdead, [72057594037927936] = 0xbeef};
- ^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^
120 #endif
121 #ifdef ARRAY_INIT4
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.16.res.oracle b/tests/syntax/oracle/very_large_integers.16.res.oracle
index eb45cfee5dbeda5a8364396ad9a361c61674cafc..f292ca3c683a39dd65d48a16e757b21d68545b05 100644
--- a/tests/syntax/oracle/very_large_integers.16.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.16.res.oracle
@@ -9,7 +9,7 @@
121 #ifdef ARRAY_INIT4
122 // Previously caused Out of memory
123 int ai4[] = {1, [7205759403792793] = 11};
- ^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^
124 #endif
125
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 8fd8c4b251b674d680d7030fb0d834a073f4db09..b72cb2ce3d3125db17c085a63e7fdc88d3a091d2 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -6,7 +6,7 @@
47 void case_range() {
48 switch (nondetul)
49 case 0 ... 9999999999999999999U:;
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
50 case 0 ... 199999999999999999U:;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index f36fb4343d810e2291e94fe870879b536f7a8698..2659f34187783f6f3f32c31b89c229f75ee37083 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -4,7 +4,7 @@
55 void case_range2() {
56 switch (nondet)
57 case 0 ... 10000000U:;
- ^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^
58 }
59 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index 0e84fc8e48cfe064978ae9009f0990872c8857f9..71b8acde63287df8b59e062509a2375eb2b3a5a3 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -4,7 +4,7 @@
64
65 #ifdef INIT_DESIGNATOR2
66 int arr3[1] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^
67 #endif
68
[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 8ccccb3e43634dfae541b21c6c3e1429bc8fbc48..09dedc1be826a7b75581602889a0d57cb6d51155 100644
--- a/tests/syntax/oracle/wrong_label.res.oracle
+++ b/tests/syntax/oracle/wrong_label.res.oracle
@@ -5,6 +5,6 @@
9
10 void main() {
11 {_LOR:} // KO: labels can't be at the end of a block.
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
12 }
[kernel] Frama-C aborted: invalid user input.