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 29107af42c7dae2bd02c1227d84c41aa7ae1d49e..2f73f4861d292bd2d53afd0a82950ece2218adce 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 52fc93d152f1d35a5c6fdd29813409959f970f2f..9f1cadaeda1e6cb9a878e27c86ec298de901ba4a 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 cc9dd69361cebc540be420b6af32ce530e359554..7cf8d6794e54f9db0f34ab6c971cc92e013fdfda 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 90d93f2d1bb5e8930d15c6c0c8ce0ddc19a3c96a..d248d992117a3356a05f6650b8b697fc7f1b390c 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 a9206db379316226e98f6f02494b78f08feb2f8c..331dfe8055508ad7a774b077b8d7b4f0d0ec88e9 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 51a45e8153f2a2dac9c507ac7483db89364bae31..909322412f84fc085ec941eaeb91d24b853f3097 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 d3d88774926a89d4af95ef421961e739ba2853e0..0eca364b644783f7bffc52806e552a4d1ac4eb80 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 f9ad299dccb537d63ffa41e43d204a37bdc62b0c..4bcdf11602646662df1553ed1c6d4b60bd297b50 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 2061e23ca869ac84660f0ba2704e5bca279fe7a2..e5c2f208daa0da69b050079e2917b19e417fc40d 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 d4ceba5f88073c917826a5eb07b90656b8b795a3..c9a7358f4566c0270e4791daa63e7ad53f418c22 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 70440cb9add4310a4a1ea79dd5effd17601561eb..be41ccba392c0bd388deb229d5445de58697539f 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 2e31db1b1a353f3252419437003a2204c9cfe910..256d77be54eea88d5de89856edfa865ae4cd8abf 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 256825a239562a0d621c9e444b30c01ddf3bee99..09ba17a47e269d5a40446c613f67d7d35cd6f4fd 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 b02fa18dfca397032322b5c91e907594e045e1eb..c7f469245aac2f5886c75f2c58a7eb60686423c4 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 be000a089fbcb883cd047675088cad92fcd86628..b59e250637e626f65af0409a1c6d59a54cfa8967 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 c42acf52d3d7944c99f1f5240f507a9522dc5fac..58485345dabdc136537c19176ff04969de2a8e4f 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 700ebc08a678c69a7d5d096eb14bb100d87b2553..afda7c511b52ec0574f6ba09878c309ffc49aac0 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 8e85e94b61f9a6a6ce89a04bacefd41f0dd47ad1..abedc4ec18bd0fd06ea9bac40407d8aa9c57ae26 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 de301e075c4f5f563d7b6ca71c214c229916561f..35b7a148eb975f2de2aba45c97a7c741df1d3ab6 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 cf05405d419277bb7d2b0ed2d58efa5abaac42dd..218315e21b14ed0d0a190d1042df3801383989b1 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 bb2402ea2df5ca18cf03af89d624060ca48eda63..0fc570c7b670da969e4e103274aa5a031fa77d53 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 cb9c57ef014b83449b763e5d64c049e3fbf7d4f4..880f1b230eb0b5c44e5c6b09bc3c209c356842c9 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 e651a1f30d1bb0457441c4546458cec0df9e4e21..507ff0d508144acc5759a7f2a9199a02ecaf923a 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 038ab482208c4f531c62dc10d5e6c86f1d9c1e49..fa6f9af638d0448cc55fd8c5a71071d0c5d2b33d 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 aaee700de3e0333d391e2524439b518ab3b5d152..c3c07133fcb3d67d7d06f4b10da5c418e22dc0ef 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 67303a701fca626253759917c6a8d7ef31be47fa..2dc9215a35ac450654652550a7134ac578f0d973 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 79768f7799b608b775963b5a3463710cdcb47635..23e5bce2386bd9bb6e8994cb30b9b89d71e63abf 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 0ae872708907a5410141a74efc231c127126d7e8..e1fc81de7638961470872331b6a7e2ace1f35cef 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 395f59284a48ac86eca556a12c95f23a5078c816..6149ca6c14a7ef7f6b9b4cb653bace5472af8f22 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 349d3259223c8124771466cdf8c806797e50d91a..75d299175cdf14a4c23369123383d94c83412930 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 7d532fb832d1b38c4f5eba24de67bdaf9429055c..1eac0647def6c209d2ae35d2137f82a76bcaecde 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 8b2cbafb4be762a70b9261856c921a8cad111f23..b3cdb439097d9a71eb9889b5b6af3246fcae9ab1 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 ac8b8986e6126c819b7412eff41c18a4f2996bf7..97bc6f5808c4546a36098776a764a2b82d62c921 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 5fb813906374f4df81a6f8630228173173c874dc..e683c048013d632828688464c432aacd535c1d5c 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 06745b8eff7a79888d135d068ba2a2382e3af97c..f1c86c668f3b5d44078dd2fad20ee3189ae350f2 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 9444a17ed88ec5d10781b6407733a909a281e0b3..47db165e125863871e8aa11d51329b948954a9ff 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 39ae93565ee58450a2185521c99ea35ac4297e2f..17b9dbce578c02ed0e29a79f18e4a5cc97fe53bb 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 d227d8bcfa84008588cc41c69532d976694a8a51..b8635912296f2a8ab067e16ae5cd6c79e617740a 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 246eb1271e90acbdd34e4b25249bab42111acad9..8c7597d919f243915e628427efbabb963df4021e 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 57c902ce64109423221b2ac4549779ced28c6ac2..db076a7b7a6ec433049a8b98e4ce8eb693c051ac 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 572b103f6576e2c2116cbfbf3dfe19d8782cbbd9..e93176c3f51050fa4a63b0faffdb54c3ec86b17f 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 90b72170fcc9f536e237d1c1c662917ad1d93acf..bbd65eb1a6faa0092073140988767f7ab8f59b31 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 2acfe9b1216851939fffe2562d227e809f7ec50b..51ba9929f8136b5cb1cc74d0c293a6aca4f25e4c 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 4379a28b8ec3d08c4ce1410e0c1c8927c59dca21..3d1e0550a28df50bbbfdbfe592a846c7fc658a3a 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 5449a4e5aacbc89c6687c57c9c2a2f802ed0d673..9f9d451cca4d7a3cb7ba454de014cce162e20a84 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 d65c73123d27fe5d752923b29fd328963b8e80ff..095cbbd26b45e686cc725c04319438085c845161 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 d57027d0548b64df6e5ebcfa632f91be0a47bce9..d94f2aee4c876a243e9e5420d33fa3611a921a75 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 26411685a8c8cf7a7dc2f6b55cb1f2414f010b5f..dae1c5e043d6ea0136c04c3a735b63efe7690ae2 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 05de919ae9493709d8edcdb77ca56d9fbe6b1f4b..30443d6f1138945a5113952ee3796e16f6f18afd 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 3e51ebdaa456a0fa941b26e6019ab42a849628be..ba34ee79c97c3cfffa2603e84dcea6d13a54b0e3 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 b8630c35e686a33525edd5eb942e9e31e40823dc..f2fe46a7218f4e48596c2a96c4773d15971234f6 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 e6f5ae2cabb16430305fec531d98c1196b11ddbd..91706e15eaf26f9bedcea422d359921b82289b31 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 e73981b6db9aa1e4866e35dc465a274599811243..366eb65da8bebad673e81287f1547ce7ba696a8c 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 77e3001832f3fffce7a42c39418da1543e2de672..35cfc826665ee35836dba7b90ce92b099648f190 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 a9c695ad6053e80c0eb1e5012cfba1c1c84787fd..d75f41a1ba1dad33bb8bca4163eab7f693a6d10e 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 95be709663e7dba8fb82dce4d6f38c2f8352f998..f38741556ecfae1c1e706ec18f985659d0687909 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 7a97e9e13450989c791b491a34f937a538ea041b..a43dffc8a880f058bfef52ebfded61cdad2cde23 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 e337a6d1b342426bc1f0b268bd698f1624defba6..932ba6a9399444dec741181df9db902b126368a9 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 6ee660e6d8fcd27361ef8329290639f1a457bbc4..c3a946c73e7cff7cd41935da87661bed4453c4c2 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 bf15241312d684a7311bfd09daeac51cb9847523..76603c68330d472624936e438e76176d33c1e163 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 59a23d5943d4402ddb9910634e73328bcf264b59..177b11f83f9963da63cc7a8b11fde507a1181387 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 74ab8ae4929831eabb086c70a64621a0a51abc77..ced390c66571f2674008b9e632de4e4601b8aed4 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 9f48a481b14d8c7fa5a5e78205a394a884da326d..310c659fa41b8b24138c150f6615c563508c9994 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 218a813f0dcc5e06354b8cf2dedee06c5f348cba..36eadea81f3b5b6bd52fb3eb0797126e9bfe2d4f 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 62c679be0ae5756391eec4fe90a5beba69b077df..279e77e82b0a80efa541243786ebfbbf0a8f6e85 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 3cc52c6d29e9e2c7397e635d39563599327c5efc..e366b8133a7e85112801a124416854e98bebead7 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 b40b28536c462ed1cdf6e67e9bd4a8662508186b..2ad84d77204218912477e33a003703ac20ce4ce7 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 3a4a0c0b8384464f300e6e536aa0a235f44df597..baa5289f5572f4aa93d8eb04ac649a6b2bb3887d 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 8d7684b496fc3074cacf1497a58a1b93f44243ed..258dd40268376ba56fbcb9483b044db1419715b2 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 adad50468228f08fd7b086a7df5e94d996d82dbe..c8f36fffabbea0ea7fb9e8339e9582d4c8feefef 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 1d8fc3c7d7c010cb51c88aa883b1d8d7426f8e48..773cecaac1fd5f1a4faf437574f6578214519a23 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 851e81eb0347ab34fc53a305992e740c3faed63b..999706dea413ac6c5c63956a666e93586569bb94 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 b46e1c5c2cdc38eb7172f8fac3c72b50af75f6c1..7c9ba7c178fdb4909990ec08bd4d6dcf11caf537 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 5e6c8b87f5192cbca50ffe3fb8ef83cb69bb860b..ca9b712f16e76c21ccb54af94f7894a05433dd92 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 4d011e9d84409f07345491a9d08de690be085027..2dd40615234abca06fe729a6f9805df6005aebe3 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 c603644b586085db6acb633701ae40c06a261e5f..8858cc405bb0645d7f38002cae3026c63d295700 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 5ca8f61644c59e35ad6866a23f53a401e46009c8..22ddabcd753fb60429538a5af7d37fb3174b8581 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 2c2a6cbdf3ab7e69653f75f37b88839bf91fe53d..dd5b469d1be2e225d142f3cc3d4a8f65493e6c88 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 0fadb7b2d67e9ffb2da7f4a1dea200b3b5931d8b..85766b5401ffebf7cee24786897212ae7241fedc 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 5ed5a2552d7bdc8bf214e134b0f66d1bb4b00e55..62bce111ca998c475103f11cedc7d16c75c6b07a 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 019c09a82d65b2fb085b5c5523accd75088742c0..eb0f8ece4e0737806ec80e0a2bea560d2eddb641 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.