From fced35089c4bdac10b1b0effb0b76ca4e75ff5d4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Jan 2024 18:35:30 +0100
Subject: [PATCH] [kernel] Better API for Errorloc.pp_context_from_file
---
src/kernel_internals/parsing/errorloc.ml | 20 +++++++++----------
src/kernel_internals/parsing/errorloc.mli | 13 ++++++------
src/kernel_internals/typing/cabs2cil.ml | 5 ++---
src/plugins/aorai/utils_parser.ml | 15 +++++++-------
src/plugins/aorai/utils_parser.mli | 4 ----
tests/misc/oracle/bts0451.res.oracle | 2 +-
tests/syntax/localisation_error.i | 4 ++++
tests/syntax/oracle/arg_type.res.oracle | 2 +-
tests/syntax/oracle/binary_op.0.res.oracle | 2 +-
tests/syntax/oracle/binary_op.1.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.0.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.3.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.4.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.5.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.6.res.oracle | 2 +-
.../oracle/const-assignments.1.res.oracle | 2 +-
.../oracle/const-assignments.2.res.oracle | 2 +-
.../oracle/const-assignments.3.res.oracle | 2 +-
.../oracle/const-assignments.4.res.oracle | 2 +-
.../oracle/const-assignments.5.res.oracle | 2 +-
.../oracle/const-assignments.6.res.oracle | 2 +-
.../oracle/const-assignments.9.res.oracle | 2 +-
.../oracle/function_ptr_lvalue_1.res.oracle | 2 +-
.../oracle/function_ptr_lvalue_2.res.oracle | 2 +-
tests/syntax/oracle/generic.1.res.oracle | 2 +-
tests/syntax/oracle/generic.2.res.oracle | 2 +-
tests/syntax/oracle/generic.3.res.oracle | 2 +-
tests/syntax/oracle/generic.4.res.oracle | 5 ++++-
tests/syntax/oracle/generic.5.res.oracle | 5 ++++-
tests/syntax/oracle/generic.6.res.oracle | 2 +-
tests/syntax/oracle/generic.7.res.oracle | 2 +-
tests/syntax/oracle/generic.8.res.oracle | 2 +-
.../ghost_cv_parsing_errors.0.res.oracle | 2 +-
.../ghost_cv_parsing_errors.1.res.oracle | 2 +-
.../syntax/oracle/ghost_else_bad.0.res.oracle | 2 +-
.../oracle/ghost_local_ill_formed.res.oracle | 2 +-
.../oracle/ghost_multiline_annot.3.res.oracle | 2 +-
.../oracle/ghost_parameters.11.res.oracle | 2 +-
...nconsistent_global_ghost_spec.0.res.oracle | 2 +-
...nconsistent_global_ghost_spec.1.res.oracle | 2 +-
...nconsistent_global_ghost_spec.2.res.oracle | 2 +-
.../oracle/localisation_error.res.oracle | 0
tests/syntax/oracle/lvalvoid.res.oracle | 2 +-
tests/syntax/oracle/no_prototype.res.oracle | 2 +-
...ject_use_decl_mismatch_bts728.0.res.oracle | 2 +-
...ject_use_decl_mismatch_bts728.1.res.oracle | 2 +-
.../oracle/type_branch_bts_1081.res.oracle | 2 +-
.../typedef_namespace_bts1500.1.res.oracle | 2 +-
.../oracle/very_large_integers.13.res.oracle | 2 +-
.../oracle/very_large_integers.14.res.oracle | 2 +-
.../oracle/very_large_integers.15.res.oracle | 2 +-
.../oracle/very_large_integers.16.res.oracle | 2 +-
.../oracle/very_large_integers.2.res.oracle | 2 +-
.../oracle/very_large_integers.3.res.oracle | 2 +-
.../oracle/very_large_integers.5.res.oracle | 2 +-
tests/syntax/oracle/wrong_label.res.oracle | 2 +-
56 files changed, 86 insertions(+), 79 deletions(-)
create mode 100644 tests/syntax/localisation_error.i
create mode 100644 tests/syntax/oracle/localisation_error.res.oracle
diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml
index c1a5effb6b7..31b21bccd37 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 3d2163ab129..e067ebd1d20 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 d98f976c738..4e13f8455dd 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 52cfe20c61e..03706bd02db 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 94495b62110..65d6018cc86 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 909322412f8..0fbb9f6d610 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 00000000000..9ba065a77bc
--- /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 256d77be54e..e38a0c4a8db 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 60dc2afc775..ba9b4df4645 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 b896f4027b9..3c36f99b1ba 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 35b7a148eb9..f6a1827a00e 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 218315e21b1..2e259dde294 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 0fc570c7b67..0ede081258a 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 880f1b230eb..9d7c6211083 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 507ff0d5081..7ae19b28c59 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 fa6f9af638d..36093e3713d 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 2dc9215a35a..02f6615a1ee 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 23e5bce2386..d2d7a5d27ab 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 e1fc81de763..f773542dfc5 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 6149ca6c14a..1bc8881f49e 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 75d299175cd..0a47849f5a7 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 1eac0647def..195a2422957 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 0eca364b644..e5ce52792db 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 4bcdf116026..e8647463136 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 07cb4e0900f..68c2dc2c614 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 97bc6f5808c..0edc5626dfd 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 e683c048013..af00e69e6f9 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 f1c86c668f3..4dea267e9f5 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 47db165e125..579b9dde795 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 17b9dbce578..fbfffc1be28 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 b8635912296..c232c3c417e 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 d07d4fc7c3b..d77e640dffc 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 ccbca4666e4..556ea0b473f 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 c6e7d874a8f..1060fb309d1 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 8c7597d919f..687b31dd0c0 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 db076a7b7a6..fcab3b6edda 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 ca5a43f04dd..5abb405a768 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 27c61b15f15..481f6d94555 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 91706e15eaf..9b4dd9a9076 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 366eb65da8b..9c6cce1bd60 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 35cfc826665..e6dd04f33e9 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 00000000000..e69de29bb2d
diff --git a/tests/syntax/oracle/lvalvoid.res.oracle b/tests/syntax/oracle/lvalvoid.res.oracle
index a43dffc8a88..bca0bd16299 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 c3a946c73e7..5cebe4f9f28 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 76603c68330..8bf3f8034fb 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 177b11f83f9..1e4b063503a 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 279e77e82b0..ea64e936b23 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 382925a17d8..9a3b3fba233 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 e74ad25634d..dfa0361fdd0 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 3ded691db12..7cbdaf67c3b 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 b39f7c8df96..c50d81a831f 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 eb45cfee5db..f292ca3c683 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 8fd8c4b251b..b72cb2ce3d3 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 f36fb4343d8..2659f341877 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 0e84fc8e48c..71b8acde632 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 8ccccb3e436..09dedc1be82 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.
--
GitLab