From 969e01bc12052ede67a74b5be52f5a8669d349ee Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 28 Aug 2023 11:38:06 +0200
Subject: [PATCH] Update oracles
---
.../tests/wp_plugin/oracle/nullable_ext.1.res.oracle | 2 --
.../tests/wp_plugin/oracle/nullable_ext.2.res.oracle | 2 --
.../tests/wp_plugin/oracle/nullable_ext.3.res.oracle | 2 --
.../tests/wp_plugin/oracle/nullable_ext.4.res.oracle | 2 --
tests/cil/oracle/acsl-comments.res.oracle | 1 -
tests/misc/oracle/bts0451.res.oracle | 1 -
tests/misc/oracle/function_ptr_lvalue_1.res.oracle | 7 ++++++-
tests/misc/oracle/function_ptr_lvalue_2.res.oracle | 7 ++++++-
tests/spec/extend_extern.ml | 2 +-
tests/spec/oracle/extend_extern.res.oracle | 4 ----
tests/syntax/oracle/alloc_order.res.oracle | 1 -
tests/syntax/oracle/arg_type.res.oracle | 8 ++++++--
tests/syntax/oracle/array_cast_bts1099.res.oracle | 3 +--
tests/syntax/oracle/axiomatic_nested.res.oracle | 1 -
tests/syntax/oracle/c11-keywords.0.res.oracle | 4 +---
tests/syntax/oracle/c11-keywords.1.res.oracle | 4 +---
tests/syntax/oracle/c11-keywords.2.res.oracle | 4 +---
tests/syntax/oracle/c11-keywords.3.res.oracle | 4 +---
tests/syntax/oracle/cert_msc_38.0.res.oracle | 11 ++++++++---
tests/syntax/oracle/cert_msc_38.3.res.oracle | 11 ++++++++---
tests/syntax/oracle/cert_msc_38.4.res.oracle | 11 ++++++++---
tests/syntax/oracle/cert_msc_38.5.res.oracle | 11 ++++++++---
tests/syntax/oracle/cert_msc_38.6.res.oracle | 11 ++++++++---
tests/syntax/oracle/const-assignments.1.res.oracle | 8 ++++++--
tests/syntax/oracle/const-assignments.10.res.oracle | 2 --
tests/syntax/oracle/const-assignments.2.res.oracle | 8 ++++++--
tests/syntax/oracle/const-assignments.3.res.oracle | 8 ++++++--
tests/syntax/oracle/const-assignments.4.res.oracle | 8 ++++++--
tests/syntax/oracle/const-assignments.5.res.oracle | 8 ++++++--
tests/syntax/oracle/const-assignments.6.res.oracle | 8 ++++++--
tests/syntax/oracle/const-assignments.9.res.oracle | 8 ++++++--
tests/syntax/oracle/generic.0.res.oracle | 2 --
tests/syntax/oracle/generic.2.res.oracle | 8 ++++++--
tests/syntax/oracle/generic.3.res.oracle | 8 ++++++--
tests/syntax/oracle/generic.4.res.oracle | 8 ++++++--
tests/syntax/oracle/generic.5.res.oracle | 8 ++++++--
tests/syntax/oracle/generic.6.res.oracle | 8 ++++++--
tests/syntax/oracle/generic.7.res.oracle | 8 ++++++--
tests/syntax/oracle/ghost_else_bad.0.res.oracle | 11 ++++++++---
.../syntax/oracle/ghost_local_ill_formed.res.oracle | 6 +++++-
.../syntax/oracle/ghost_multiline_annot.4.res.oracle | 2 --
.../syntax/oracle/ghost_multiline_annot.5.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.10.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.3.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.4.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.5.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.6.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.7.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.8.res.oracle | 2 --
tests/syntax/oracle/ghost_parameters.9.res.oracle | 2 --
.../syntax/oracle/incomplete_struct_field.res.oracle | 10 ++++++++--
.../inconsistent_global_ghost_spec.0.res.oracle | 2 --
.../inconsistent_global_ghost_spec.1.res.oracle | 2 --
.../inconsistent_global_ghost_spec.2.res.oracle | 2 --
.../inconsistent_global_ghost_spec.3.res.oracle | 2 --
tests/syntax/oracle/init_bts1352.res.oracle | 1 -
tests/syntax/oracle/lvalvoid.res.oracle | 11 +++++++++--
.../oracle/mutually_recursive_struct.res.oracle | 10 ++++++++--
tests/syntax/oracle/no_prototype.res.oracle | 9 ++++++++-
.../reject_use_decl_mismatch_bts728.0.res.oracle | 2 --
.../reject_use_decl_mismatch_bts728.1.res.oracle | 2 --
.../oracle/struct_with_invalid_field.2.res.oracle | 2 --
.../oracle/struct_with_invalid_field.3.res.oracle | 2 --
tests/syntax/oracle/syntactic_hook.res.oracle | 1 -
tests/syntax/oracle/type_branch_bts_1081.res.oracle | 9 +++++++--
tests/syntax/oracle/very_large_integers.0.res.oracle | 2 --
.../syntax/oracle/very_large_integers.10.res.oracle | 4 +---
.../syntax/oracle/very_large_integers.13.res.oracle | 8 ++++++--
.../syntax/oracle/very_large_integers.14.res.oracle | 8 ++++++--
.../syntax/oracle/very_large_integers.15.res.oracle | 8 ++++++--
.../syntax/oracle/very_large_integers.16.res.oracle | 8 ++++++--
tests/syntax/oracle/very_large_integers.2.res.oracle | 12 ++++++++----
tests/syntax/oracle/very_large_integers.3.res.oracle | 11 ++++++++---
tests/syntax/oracle/very_large_integers.4.res.oracle | 8 ++++++--
tests/syntax/oracle/very_large_integers.5.res.oracle | 2 --
tests/syntax/oracle/very_large_integers.6.res.oracle | 10 +++++++---
tests/syntax/oracle/very_large_integers.7.res.oracle | 11 ++++++++---
tests/syntax/oracle/very_large_integers.9.res.oracle | 4 +---
tests/syntax/oracle/wrong-assignment.res.oracle | 9 +++++++--
tests/value/oracle/array_zero_length.2.res.oracle | 1 -
tests/value/oracle/empty_base.1.res.oracle | 2 --
81 files changed, 265 insertions(+), 169 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle
index 29107af42c7..2f73f4861d2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle
@@ -3,6 +3,4 @@
[kernel:annot-error] nullable_ext.c:51: Warning:
unbound logic variable unexisting_ptr. Ignoring logic specification of function fails_no_variable
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "nullable_ext.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle
index 52fc93d152f..9f1cadaeda1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle
@@ -3,6 +3,4 @@
[kernel:annot-error] nullable_ext.c:58: Warning:
Not a formal pointer: *ptr. Ignoring logic specification of function not_a_variable
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "nullable_ext.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle
index cc9dd69361c..7cf8d6794e5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle
@@ -3,6 +3,4 @@
[kernel:annot-error] nullable_ext.c:65: Warning:
Not a formal pointer: g. Ignoring logic specification of function not_a_formal
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "nullable_ext.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle
index 90d93f2d1bb..d248d992117 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle
@@ -3,6 +3,4 @@
[kernel:annot-error] nullable_ext.c:72: Warning:
Not a formal pointer: f. Ignoring logic specification of function not_a_pointer
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "nullable_ext.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/cil/oracle/acsl-comments.res.oracle b/tests/cil/oracle/acsl-comments.res.oracle
index a9206db3793..331dfe80555 100644
--- a/tests/cil/oracle/acsl-comments.res.oracle
+++ b/tests/cil/oracle/acsl-comments.res.oracle
@@ -2,5 +2,4 @@
[kernel:annot-error] acsl-comments.i:6: Warning:
lexical error, unexpected block-comment opening
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "acsl-comments.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/bts0451.res.oracle b/tests/misc/oracle/bts0451.res.oracle
index 51a45e8153f..909322412f8 100644
--- a/tests/misc/oracle/bts0451.res.oracle
+++ b/tests/misc/oracle/bts0451.res.oracle
@@ -7,5 +7,4 @@
^^^^^^^^
28 return 0;
29 }
-[kernel] User Error: stopping on file "bts0451.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_lvalue_1.res.oracle b/tests/misc/oracle/function_ptr_lvalue_1.res.oracle
index d3d88774926..0eca364b644 100644
--- a/tests/misc/oracle/function_ptr_lvalue_1.res.oracle
+++ b/tests/misc/oracle/function_ptr_lvalue_1.res.oracle
@@ -1,5 +1,10 @@
[kernel] Parsing function_ptr_lvalue_1.i (no preprocessing)
[kernel] function_ptr_lvalue_1.i:13: User Error:
Cannot assign to non-modifiable lval *p
-[kernel] User Error: stopping on file "function_ptr_lvalue_1.i" that has errors.
+ 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/misc/oracle/function_ptr_lvalue_2.res.oracle b/tests/misc/oracle/function_ptr_lvalue_2.res.oracle
index f9ad299dccb..4bcdf116026 100644
--- a/tests/misc/oracle/function_ptr_lvalue_2.res.oracle
+++ b/tests/misc/oracle/function_ptr_lvalue_2.res.oracle
@@ -1,5 +1,10 @@
[kernel] Parsing function_ptr_lvalue_2.i (no preprocessing)
[kernel] function_ptr_lvalue_2.i:12: User Error:
Cannot assign to non-modifiable lval *p
-[kernel] User Error: stopping on file "function_ptr_lvalue_2.i" that has errors.
+ 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/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index 2061e23ca86..e5c2f208daa 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -25,7 +25,7 @@ let main () =
"Checking handler of exception occurring in extension typing";
Ast.compute (); assert false
with
- | Log.AbortError _ -> Kernel.feedback "Extension typing failed as expected"
+ | Log.AbortFatal _ -> Kernel.feedback "Extension typing failed as expected"
| Not_found -> Kernel.fatal "kernel did not capture our exception"
| Assert_failure _ -> Kernel.fatal "kernel silently captured our exception"
diff --git a/tests/spec/oracle/extend_extern.res.oracle b/tests/spec/oracle/extend_extern.res.oracle
index d4ceba5f880..c9a7358f456 100644
--- a/tests/spec/oracle/extend_extern.res.oracle
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -1,8 +1,4 @@
[kernel] Checking handler of exception occurring in extension typing
[kernel] Parsing extend_extern.i (no preprocessing)
[kernel] Failure: Typechecking ACSL extension why3 raised exception Not_found
-[kernel:annot-error] extend_extern.i:6: Warning:
- Logic typing error. Ignoring global annotation
-[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "extend_extern.i" that has errors.
[kernel] Extension typing failed as expected
diff --git a/tests/syntax/oracle/alloc_order.res.oracle b/tests/syntax/oracle/alloc_order.res.oracle
index 70440cb9add..be41ccba392 100644
--- a/tests/syntax/oracle/alloc_order.res.oracle
+++ b/tests/syntax/oracle/alloc_order.res.oracle
@@ -2,5 +2,4 @@
[kernel:annot-error] alloc_order.i:8: Warning:
wrong order of clause in contract: requires after post-condition, assigns or allocates.
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "alloc_order.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/arg_type.res.oracle b/tests/syntax/oracle/arg_type.res.oracle
index 2e31db1b1a3..256d77be54e 100644
--- a/tests/syntax/oracle/arg_type.res.oracle
+++ b/tests/syntax/oracle/arg_type.res.oracle
@@ -2,6 +2,10 @@
[kernel] arg_type.i:15: User Error:
Declaration of g does not match previous declaration from arg_type.i:13 (different integer types:
'int' and 'short').
-[kernel] arg_type.i:15: User Error: Cannot resolve variable x
-[kernel] User Error: stopping on file "arg_type.i" that has errors.
+[kernel] arg_type.i:15: User Error:
+ Cannot resolve variable x
+ 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/array_cast_bts1099.res.oracle b/tests/syntax/oracle/array_cast_bts1099.res.oracle
index 256825a2395..09ba17a47e2 100644
--- a/tests/syntax/oracle/array_cast_bts1099.res.oracle
+++ b/tests/syntax/oracle/array_cast_bts1099.res.oracle
@@ -1,10 +1,9 @@
[kernel] Parsing array_cast_bts1099.i (no preprocessing)
[kernel] array_cast_bts1099.i:12: User Error:
- Cast over a non-scalar type t
+ explicit cast: cast over a non-scalar type t
10 int tab1[4];
11 u* p = &tab1;
12 t* p2 = (t) p;
^^^^^^^^^^^^^^^^
13 }
-[kernel] User Error: stopping on file "array_cast_bts1099.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/axiomatic_nested.res.oracle b/tests/syntax/oracle/axiomatic_nested.res.oracle
index b02fa18dfca..c7f469245aa 100644
--- a/tests/syntax/oracle/axiomatic_nested.res.oracle
+++ b/tests/syntax/oracle/axiomatic_nested.res.oracle
@@ -2,5 +2,4 @@
[kernel:annot-error] axiomatic_nested.i:8: Warning:
Nested axiomatic. Ignoring body of bla2. Ignoring global annotation
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "axiomatic_nested.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/c11-keywords.0.res.oracle b/tests/syntax/oracle/c11-keywords.0.res.oracle
index be000a089fb..b59e250637e 100644
--- a/tests/syntax/oracle/c11-keywords.0.res.oracle
+++ b/tests/syntax/oracle/c11-keywords.0.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing c11-keywords.c (with preprocessing)
-[kernel] c11-keywords.c:11: Failure:
+[kernel] c11-keywords.c:11: User Error:
_Alignas is currently unsupported by Frama-C.
-[kernel] User Error: stopping on file "c11-keywords.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/c11-keywords.1.res.oracle b/tests/syntax/oracle/c11-keywords.1.res.oracle
index c42acf52d3d..58485345dab 100644
--- a/tests/syntax/oracle/c11-keywords.1.res.oracle
+++ b/tests/syntax/oracle/c11-keywords.1.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing c11-keywords.c (with preprocessing)
-[kernel] c11-keywords.c:17: Failure:
+[kernel] c11-keywords.c:17: User Error:
_Alignof is currently unsupported by Frama-C.
-[kernel] User Error: stopping on file "c11-keywords.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/c11-keywords.2.res.oracle b/tests/syntax/oracle/c11-keywords.2.res.oracle
index 700ebc08a67..afda7c511b5 100644
--- a/tests/syntax/oracle/c11-keywords.2.res.oracle
+++ b/tests/syntax/oracle/c11-keywords.2.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing c11-keywords.c (with preprocessing)
-[kernel] c11-keywords.c:21: Failure:
+[kernel] c11-keywords.c:21: User Error:
_Complex is currently unsupported by Frama-C.
-[kernel] User Error: stopping on file "c11-keywords.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/c11-keywords.3.res.oracle b/tests/syntax/oracle/c11-keywords.3.res.oracle
index 8e85e94b61f..abedc4ec18b 100644
--- a/tests/syntax/oracle/c11-keywords.3.res.oracle
+++ b/tests/syntax/oracle/c11-keywords.3.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing c11-keywords.c (with preprocessing)
-[kernel] c11-keywords.c:26: Failure:
+[kernel] c11-keywords.c:26: User Error:
_Imaginary is currently unsupported by Frama-C.
-[kernel] User Error: stopping on file "c11-keywords.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[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 de301e075c4..35b7a148eb9 100644
--- a/tests/syntax/oracle/cert_msc_38.0.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.0.res.oracle
@@ -1,7 +1,12 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:26: Warning:
assert is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] cert_msc_38.c:26: User Error: Cannot resolve variable assert
-[kernel] User Error: stopping on file "cert_msc_38.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+[kernel] cert_msc_38.c:26: User Error:
+ Cannot resolve variable assert
+ 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 cf05405d419..218315e21b1 100644
--- a/tests/syntax/oracle/cert_msc_38.3.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.3.res.oracle
@@ -1,7 +1,12 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:43: Warning:
va_start is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] cert_msc_38.c:43: User Error: Cannot resolve variable va_start
-[kernel] User Error: stopping on file "cert_msc_38.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+[kernel] cert_msc_38.c:43: User Error:
+ Cannot resolve variable va_start
+ 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 bb2402ea2df..0fc570c7b67 100644
--- a/tests/syntax/oracle/cert_msc_38.4.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.4.res.oracle
@@ -1,7 +1,12 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:47: Warning:
va_copy is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] cert_msc_38.c:47: User Error: Cannot resolve variable va_copy
-[kernel] User Error: stopping on file "cert_msc_38.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+[kernel] cert_msc_38.c:47: User Error:
+ Cannot resolve variable va_copy
+ 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 cb9c57ef014..880f1b230eb 100644
--- a/tests/syntax/oracle/cert_msc_38.5.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.5.res.oracle
@@ -1,7 +1,12 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:51: Warning:
va_arg is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] cert_msc_38.c:51: User Error: Cannot resolve variable va_arg
-[kernel] User Error: stopping on file "cert_msc_38.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+[kernel] cert_msc_38.c:51: User Error:
+ Cannot resolve variable va_arg
+ 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 e651a1f30d1..507ff0d5081 100644
--- a/tests/syntax/oracle/cert_msc_38.6.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.6.res.oracle
@@ -1,7 +1,12 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:55: Warning:
va_end is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] cert_msc_38.c:55: User Error: Cannot resolve variable va_end
-[kernel] User Error: stopping on file "cert_msc_38.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+[kernel] cert_msc_38.c:55: User Error:
+ Cannot resolve variable va_end
+ 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 038ab482208..fa6f9af638d 100644
--- a/tests/syntax/oracle/const-assignments.1.res.oracle
+++ b/tests/syntax/oracle/const-assignments.1.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:22: User Error:
Cannot assign to non-modifiable lval x
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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.10.res.oracle b/tests/syntax/oracle/const-assignments.10.res.oracle
index aaee700de3e..c3c07133fcb 100644
--- a/tests/syntax/oracle/const-assignments.10.res.oracle
+++ b/tests/syntax/oracle/const-assignments.10.res.oracle
@@ -2,6 +2,4 @@
[kernel:typing:incompatible-types-call] const-assignments.c:110: Warning:
expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
[kernel] User Error: warning typing:incompatible-types-call treated as fatal error.
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 67303a701fc..2dc9215a35a 100644
--- a/tests/syntax/oracle/const-assignments.2.res.oracle
+++ b/tests/syntax/oracle/const-assignments.2.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:28: User Error:
Cannot assign to non-modifiable lval x
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 79768f7799b..23e5bce2386 100644
--- a/tests/syntax/oracle/const-assignments.3.res.oracle
+++ b/tests/syntax/oracle/const-assignments.3.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:34: User Error:
Cannot assign to non-modifiable lval x
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 0ae87270890..e1fc81de763 100644
--- a/tests/syntax/oracle/const-assignments.4.res.oracle
+++ b/tests/syntax/oracle/const-assignments.4.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:40: User Error:
Cannot assign to non-modifiable lval x
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 395f59284a4..6149ca6c14a 100644
--- a/tests/syntax/oracle/const-assignments.5.res.oracle
+++ b/tests/syntax/oracle/const-assignments.5.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:47: User Error:
Cannot assign to non-modifiable lval x_0
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 349d3259223..75d299175cd 100644
--- a/tests/syntax/oracle/const-assignments.6.res.oracle
+++ b/tests/syntax/oracle/const-assignments.6.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:53: User Error:
Cannot assign to non-modifiable lval *x_0
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 7d532fb832d..1eac0647def 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel] const-assignments.c:121: User Error:
Cannot assign to non-modifiable lval t->s.y
-[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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/generic.0.res.oracle b/tests/syntax/oracle/generic.0.res.oracle
index 8b2cbafb4be..b3cdb439097 100644
--- a/tests/syntax/oracle/generic.0.res.oracle
+++ b/tests/syntax/oracle/generic.0.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel:c11] Warning: _Generic is a C11 keyword
[kernel] User Error: warning c11 treated as fatal error.
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[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 ac8b8986e61..97bc6f5808c 100644
--- a/tests/syntax/oracle/generic.2.res.oracle
+++ b/tests/syntax/oracle/generic.2.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel] generic.c:39: User Error:
multiple default clauses in _Generic selection
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+ 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 5fb81390637..e683c048013 100644
--- a/tests/syntax/oracle/generic.3.res.oracle
+++ b/tests/syntax/oracle/generic.3.res.oracle
@@ -2,6 +2,10 @@
[kernel] generic.c:43: User Error:
multiple compatible types in _Generic selection:
'my_uint' and 'unsigned int'
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+ 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 06745b8eff7..f1c86c668f3 100644
--- a/tests/syntax/oracle/generic.4.res.oracle
+++ b/tests/syntax/oracle/generic.4.res.oracle
@@ -2,6 +2,10 @@
[kernel] generic.c:47: User Error:
multiple compatible types in _Generic selection:
'void (*)()' and 'void (*)(void)'
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+ 45 #ifdef TOO_MANY_COMPATIBLE2
+ 46 // compatibility modulo implicit arguments
+ 47 int a = _Generic(0,
+ ^^^^^^^^^^^^^^^^^^^^^
+ 48 void (*)(): 0,
+ 49 void (*)(void): 0);
[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 9444a17ed88..47db165e125 100644
--- a/tests/syntax/oracle/generic.5.res.oracle
+++ b/tests/syntax/oracle/generic.5.res.oracle
@@ -3,6 +3,10 @@
controlling expression compatible with more than one association type in _Generic selection:
controlling expression: '(void (*)())0' (type: void (*)());
compatible types: void (*)(void), void (*)(int )
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+ 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);
[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 39ae93565ee..17b9dbce578 100644
--- a/tests/syntax/oracle/generic.6.res.oracle
+++ b/tests/syntax/oracle/generic.6.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel] generic.c:59: User Error:
generic association with incomplete type 'void'
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+ 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 d227d8bcfa8..b8635912296 100644
--- a/tests/syntax/oracle/generic.7.res.oracle
+++ b/tests/syntax/oracle/generic.7.res.oracle
@@ -3,6 +3,10 @@
no compatible types and no default type in _Generic selection:
controlling expression: '"abc"' (type: char *);
candidate types: char const *
-[kernel] User Error: stopping on file "generic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+ 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/ghost_else_bad.0.res.oracle b/tests/syntax/oracle/ghost_else_bad.0.res.oracle
index 246eb1271e9..8c7597d919f 100644
--- a/tests/syntax/oracle/ghost_else_bad.0.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.0.res.oracle
@@ -1,5 +1,10 @@
[kernel] Parsing ghost_else_bad.c (with preprocessing)
-[kernel] ghost_else_bad.c:20: User Error: Cannot resolve variable z
-[kernel] User Error: stopping on file "ghost_else_bad.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
+[kernel] ghost_else_bad.c:20: User Error:
+ Cannot resolve variable z
+ 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 57c902ce641..db076a7b7a6 100644
--- a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
+++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
@@ -4,5 +4,9 @@
Previous declaration was at ghost_local_ill_formed.i:6
[kernel] ghost_local_ill_formed.i:21: User Error:
Variable c is a ghost symbol. It cannot be used in non-ghost context. Did you forget a /*@ ghost ... /?
-[kernel] User Error: stopping on file "ghost_local_ill_formed.i" that has errors.
+ 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.4.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.4.res.oracle
index 572b103f657..e93176c3f51 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.4.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.4.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
[kernel:annot-error] ghost_multiline_annot.c:65: Warning: unexpected token '/'
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "ghost_multiline_annot.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_multiline_annot.5.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.5.res.oracle
index 90b72170fcc..bbd65eb1a6f 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.5.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.5.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
[kernel:annot-error] ghost_multiline_annot.c:76: Warning: unexpected token '/'
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "ghost_multiline_annot.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.10.res.oracle b/tests/syntax/oracle/ghost_parameters.10.res.oracle
index 2acfe9b1216..51ba9929f81 100644
--- a/tests/syntax/oracle/ghost_parameters.10.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.10.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
188
189 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.3.res.oracle b/tests/syntax/oracle/ghost_parameters.3.res.oracle
index 4379a28b8ec..3d1e0550a28 100644
--- a/tests/syntax/oracle/ghost_parameters.3.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.3.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
93
94 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.4.res.oracle b/tests/syntax/oracle/ghost_parameters.4.res.oracle
index 5449a4e5aac..9f9d451cca4 100644
--- a/tests/syntax/oracle/ghost_parameters.4.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.4.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
107
108 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.5.res.oracle b/tests/syntax/oracle/ghost_parameters.5.res.oracle
index d65c73123d2..095cbbd26b4 100644
--- a/tests/syntax/oracle/ghost_parameters.5.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.5.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
120
121 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.6.res.oracle b/tests/syntax/oracle/ghost_parameters.6.res.oracle
index d57027d0548..d94f2aee4c8 100644
--- a/tests/syntax/oracle/ghost_parameters.6.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.6.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
134
135 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.7.res.oracle b/tests/syntax/oracle/ghost_parameters.7.res.oracle
index 26411685a8c..dae1c5e043d 100644
--- a/tests/syntax/oracle/ghost_parameters.7.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.7.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
147
148 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.8.res.oracle b/tests/syntax/oracle/ghost_parameters.8.res.oracle
index 05de919ae94..30443d6f113 100644
--- a/tests/syntax/oracle/ghost_parameters.8.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.8.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
161
162 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.9.res.oracle b/tests/syntax/oracle/ghost_parameters.9.res.oracle
index 3e51ebdaa45..ba34ee79c97 100644
--- a/tests/syntax/oracle/ghost_parameters.9.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.9.res.oracle
@@ -9,6 +9,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
174
175 }
-[kernel] User Error: stopping on file "ghost_parameters.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/incomplete_struct_field.res.oracle b/tests/syntax/oracle/incomplete_struct_field.res.oracle
index b8630c35e68..f2fe46a7218 100644
--- a/tests/syntax/oracle/incomplete_struct_field.res.oracle
+++ b/tests/syntax/oracle/incomplete_struct_field.res.oracle
@@ -3,6 +3,12 @@
declaration of array of incomplete type 'struct _s`
[kernel] incomplete_struct_field.i:7: User Error:
field `v' is declared with incomplete type struct _s [12]
-[kernel] incomplete_struct_field.i:5: User Error: type struct _s is circular
-[kernel] User Error: stopping on file "incomplete_struct_field.i" that has errors.
+[kernel] incomplete_struct_field.i:5: User Error:
+ type struct _s is circular
+ 3 STDOPT:
+ 4 */
+ 5 typedef struct _s {
+ ^^^^^^^^^^^^^^^^^^^
+ 6 int i;
+ 7 struct _s v[12];
[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 e6f5ae2cabb..91706e15eaf 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
@@ -8,6 +8,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12
13 void user(void){
-[kernel] User Error: stopping on file "inconsistent_global_ghost_spec.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 e73981b6db9..366eb65da8b 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
@@ -8,6 +8,4 @@
^^^^^^^^^^^^^^^^^^^^^^
23
24 void user(void){
-[kernel] User Error: stopping on file "inconsistent_global_ghost_spec.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 77e3001832f..35cfc826665 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
@@ -8,6 +8,4 @@
^^^^^^^^^^^^^^^^^^^^^
34
35 void user(void){
-[kernel] User Error: stopping on file "inconsistent_global_ghost_spec.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 a9c695ad605..d75f41a1ba1 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
@@ -8,6 +8,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
45
46 void user(void){
-[kernel] User Error: stopping on file "inconsistent_global_ghost_spec.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 95be709663e..f38741556ec 100644
--- a/tests/syntax/oracle/init_bts1352.res.oracle
+++ b/tests/syntax/oracle/init_bts1352.res.oracle
@@ -6,5 +6,4 @@
8 int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
9 }
-[kernel] User Error: stopping on file "init_bts1352.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/lvalvoid.res.oracle b/tests/syntax/oracle/lvalvoid.res.oracle
index 7a97e9e1345..a43dffc8a88 100644
--- a/tests/syntax/oracle/lvalvoid.res.oracle
+++ b/tests/syntax/oracle/lvalvoid.res.oracle
@@ -1,4 +1,11 @@
[kernel] Parsing lvalvoid.i (no preprocessing)
-[kernel] lvalvoid.i:8: Failure: lvalue of type void: *(src + i)
-[kernel] User Error: stopping on file "lvalvoid.i" that has errors.
+[kernel] lvalvoid.i:8: User Error:
+ lvalue of type void: *(src + i)
+
+ 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/mutually_recursive_struct.res.oracle b/tests/syntax/oracle/mutually_recursive_struct.res.oracle
index e337a6d1b34..932ba6a9399 100644
--- a/tests/syntax/oracle/mutually_recursive_struct.res.oracle
+++ b/tests/syntax/oracle/mutually_recursive_struct.res.oracle
@@ -7,6 +7,12 @@
declaration of array of incomplete type 'struct S1`
[kernel] mutually_recursive_struct.i:11: User Error:
field `s1' is declared with incomplete type struct S1 [2]
-[kernel] mutually_recursive_struct.i:11: User Error: type struct S2 is circular
-[kernel] User Error: stopping on file "mutually_recursive_struct.i" that has errors.
+[kernel] mutually_recursive_struct.i:11: User Error:
+ type struct S2 is circular
+ 9 struct S1 { struct S2 s2[2]; int x; };
+ 10
+ 11 struct S2 { struct S1 s1[2]; int y; };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 12
+ 13 int main () {
[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 6ee660e6d8f..c3a946c73e7 100644
--- a/tests/syntax/oracle/no_prototype.res.oracle
+++ b/tests/syntax/oracle/no_prototype.res.oracle
@@ -4,5 +4,12 @@
Its formals will be inferred from actual arguments
[kernel] no_prototype.i:11: User Error:
Declaration of foo does not match previous declaration from no_prototype.i:6 (different number of arguments).
-[kernel] User Error: stopping on file "no_prototype.i" that has errors.
+[kernel] no_prototype.i:11: User Error:
+ Inconsistent formals
+ 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 bf15241312d..76603c68330 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
@@ -12,6 +12,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
20 x = 17;
21 y=18;
-[kernel] User Error: stopping on file "reject_use_decl_mismatch_bts728.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 59a23d5943d..177b11f83f9 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
@@ -11,6 +11,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
20 x = 17;
21 y=18;
-[kernel] User Error: stopping on file "reject_use_decl_mismatch_bts728.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
index 74ab8ae4929..ced390c6657 100644
--- a/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
+++ b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
[kernel] struct_with_invalid_field.c:21: User Error:
negative bitfield width (-1)
-[kernel] User Error: stopping on file "struct_with_invalid_field.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
index 9f48a481b14..310c659fa41 100644
--- a/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
+++ b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
[kernel] struct_with_invalid_field.c:24: User Error:
negative bitfield width (-2147483648)
-[kernel] User Error: stopping on file "struct_with_invalid_field.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 218a813f0dc..36eadea81f3 100644
--- a/tests/syntax/oracle/syntactic_hook.res.oracle
+++ b/tests/syntax/oracle/syntactic_hook.res.oracle
@@ -44,5 +44,4 @@
29
30 int f(int); //error: conflicting decls
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-[kernel] User Error: stopping on file "syntactic_hook.i" that has errors.
[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 62c679be0ae..279e77e82b0 100644
--- a/tests/syntax/oracle/type_branch_bts_1081.res.oracle
+++ b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
@@ -1,5 +1,10 @@
[kernel] Parsing type_branch_bts_1081.i (no preprocessing)
-[kernel] type_branch_bts_1081.i:10: Failure:
+[kernel] type_branch_bts_1081.i:10: User Error:
invalid implicit conversion from void to signed char
-[kernel] User Error: stopping on file "type_branch_bts_1081.i" that has errors.
+ 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/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 3cc52c6d29e..e366b8133a7 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -3,6 +3,4 @@
integer constant too large in expression 999999999999999999U + 9999999999999999999U
[kernel] very_large_integers.c:36: User Error:
bitfield width is not a valid integer constant
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
index b40b28536c4..2ad84d77204 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -4,8 +4,6 @@
[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:97: Failure:
+[kernel] very_large_integers.c:97: User Error:
Invalid digit 9 in integer literal '09876543210' in base 8.
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[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 3a4a0c0b838..baa5289f557 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -6,6 +6,10 @@
(9223372036854775808) )
[kernel] very_large_integers.c:102: User Error:
array length too large: 72057594037927937
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 8d7684b496f..258dd402683 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -6,6 +6,10 @@
(9223372036854775808) )
[kernel] very_large_integers.c:113: User Error:
array length too large: 7205759403792794
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 111 };
+ 112 // Previously caused Out of memory
+ 113 struct st s = {
+ ^^^^^^^^^^^^^^^
+ 114 {{[7205759403792793 ... 7205759403792793] = 0}}
+ 115 };
[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 adad5046822..c8f36fffabb 100644
--- a/tests/syntax/oracle/very_large_integers.15.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -6,6 +6,10 @@
(9223372036854775808) )
[kernel] very_large_integers.c:119: User Error:
array length too large for Frama-C: 72057594037927936
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 1d8fc3c7d7c..773cecaac1f 100644
--- a/tests/syntax/oracle/very_large_integers.16.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.16.res.oracle
@@ -6,6 +6,10 @@
(9223372036854775808) )
[kernel] very_large_integers.c:123: User Error:
array length too large for Frama-C: 7205759403792793
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 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 851e81eb034..999706dea41 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -1,8 +1,12 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
[kernel] very_large_integers.c:49: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:49: Failure:
- Cannot understand the constants in case range
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] very_large_integers.c:49: User Error:
+ non-constant expression(s) in case-range
+ 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 b46e1c5c2cd..7c9ba7c178f 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,5 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:57: Failure: Case range too large
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] very_large_integers.c:57: User Error:
+ Case range too large
+ 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.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index 5e6c8b87f51..ca9b712f16e 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
[kernel] very_large_integers.c:62: User Error:
Array length 9999999999999999999U is too big: no explicit initializer allowed.
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 60
+ 61 #ifdef INIT_DESIGNATOR
+ 62 int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 63 #endif
+ 64
[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 4d011e9d844..2dd40615234 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -7,6 +7,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
67 #endif
68
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index c603644b586..8858cc405bb 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -3,8 +3,12 @@
integer constant too large in expression -9999999999999999999U
[kernel] very_large_integers.c:70: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:70: Failure:
+[kernel] very_large_integers.c:70: User Error:
INDEX_RANGE initialization designator is not a valid constant
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+ 68
+ 69 #ifdef RANGE_DESIGNATOR
+ 70 int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 71 #endif
+ 72
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 5ca8f61644c..22ddabcd753 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,5 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Failure: INDEX_RANGE too large
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] very_large_integers.c:74: User Error:
+ INDEX_RANGE too large
+ 72
+ 73 #ifdef RANGE_DESIGNATOR2
+ 74 int widths[] = { [99999999999999999 ... 999999999999999999] = 2 };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 75 #endif
+ 76
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index 2c2a6cbdf3a..dd5b469d1be 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -4,7 +4,5 @@
[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
-[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] User Error: Cannot represent logical integer in C: 9999999999999999999
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle
index 0fadb7b2d67..85766b5401f 100644
--- a/tests/syntax/oracle/wrong-assignment.res.oracle
+++ b/tests/syntax/oracle/wrong-assignment.res.oracle
@@ -1,4 +1,9 @@
[kernel] Parsing wrong-assignment.i (no preprocessing)
-[kernel] wrong-assignment.i:13: Failure: castTo ebool -> _Bool
-[kernel] User Error: stopping on file "wrong-assignment.i" that has errors.
+[kernel] wrong-assignment.i:13: User Error:
+ implicit cast: ebool -> _Bool
+ 11 void d() {
+ 12 // this assignment should be rejected
+ 13 c.a = b;
+ ^^^^^^^^^^
+ 14 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index 5ed5a2552d7..62bce111ca9 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -14,5 +14,4 @@
^^^^^^^^^^^^^^^
14 char U1[0] = {};
15 char V1[][2] = {};
-[kernel] User Error: stopping on file "array_zero_length.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index 019c09a82d6..eb0f8ece4e0 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -11,6 +11,4 @@
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
51
52 comp array_of_comp[1] = {{.a = 17, .b = 45, .e = {}}};
-[kernel] User Error: stopping on file "empty_base.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
--
GitLab