diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json index 8d1c3de1c501006d251af2aea1021d8751c5d3eb..e4a021a87048620e0f9bd7d91b11dd4756052ff7 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -67,7 +67,7 @@ "typing:int-conversion", "typing:no-proto" ], "disabled": [ - "CERT:EXP:10", "acsl-float-compare", "file:not-found", + "CERT:EXP:10", "acsl-float-compare", "c11", "file:not-found", "ghost:already-ghost", "parser:decimal-float", "transient-block" ] } diff --git a/tests/syntax/oracle/generic.0.res.oracle b/tests/syntax/oracle/generic.0.res.oracle index 57d145f153116886c4841d5ad42da57decb8ec19..8b2cbafb4be762a70b9261856c921a8cad111f23 100644 --- a/tests/syntax/oracle/generic.0.res.oracle +++ b/tests/syntax/oracle/generic.0.res.oracle @@ -1,13 +1,6 @@ [kernel] Parsing generic.c (with preprocessing) -[kernel:parser:conditional-feature] Warning: - _Generic is a C11 keyword, use -c11 option to enable it -[kernel] generic.c:67: - syntax error: - Location: line 67, between columns 28 and 32, before or at token: char - 65 int a = _Generic("abc", char const *: 0); - 66 #endif - 67 int ok1 = _Generic("abc", char*: 0); - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - 68 int ok2 = _Generic(1.0, float: 1, double: 0); - 69 int ok3 = _Generic(1L, short: 1, unsigned int: 2, int: 3, long: 0, unsigned long: 5); +[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/rename.res.oracle b/tests/syntax/oracle/rename.res.oracle index a0ff551a4ad6d61c41a1faa0d784f93478ebc316..1943c82a48286c302a8cb4351371982f32f55bf8 100644 --- a/tests/syntax/oracle/rename.res.oracle +++ b/tests/syntax/oracle/rename.res.oracle @@ -1,6 +1,4 @@ [kernel] Parsing rename.i (no preprocessing) -[kernel] rename.i:69: Warning: - unnamed fields are a C11 extension (use -c11 to avoid this warning) /* Generated by Frama-C */ struct not_anon { int __anonCompField1 ; diff --git a/tests/syntax/oracle/type_redef.0.res.oracle b/tests/syntax/oracle/type_redef.0.res.oracle deleted file mode 100644 index a27ce4063cd967341e05b9b0a4b2339109995257..0000000000000000000000000000000000000000 --- a/tests/syntax/oracle/type_redef.0.res.oracle +++ /dev/null @@ -1,81 +0,0 @@ -[kernel] Parsing type_redef.i (no preprocessing) -[kernel] type_redef.i:7: User Error: - redefinition of type 'myint' in the same scope is only allowed in C11 (option -c11). - Previous declaration was at type_redef.i:6 -[kernel] type_redef.i:10: User Error: - redefinition of type 'list' in the same scope is only allowed in C11 (option -c11). - Previous declaration was at type_redef.i:9 -[kernel] type_redef.i:13: User Error: - redefinition of type 'st' in the same scope with incompatible type. - Previous declaration was at type_redef.i:12 -[kernel] type_redef.i:18: User Error: - redefinition of type 'u' in the same scope with incompatible type. - Previous declaration was at type_redef.i:17 -[kernel] type_redef.i:21: User Error: - redefinition of 'A' in the same scope. - Previous declaration was at type_redef.i:20 -[kernel] type_redef.i:21: User Error: - redefinition of type 'e' in the same scope with conflicting type. - Previous declaration was at type_redef.i:20 -[kernel] type_redef.i:24: User Error: - redefinition of 'B' in the same scope. - Previous declaration was at type_redef.i:23 -[kernel] type_redef.i:26: User Error: - redefinition of type 'st1' in the same scope with incompatible type. - Previous declaration was at type_redef.i:15 -[kernel:parser:unsupported] type_redef.i:30: Warning: - block-level typedefs currently unsupported; - trying to convert it to a global-level typedef. - Note that this may lead to incoherent error messages. -[kernel] type_redef.i:30: Failure: - redefinition of a typedef in a non-global scope is currently unsupported -[kernel:parser:unsupported] type_redef.i:31: Warning: - block-level typedefs currently unsupported; - trying to convert it to a global-level typedef. - Note that this may lead to incoherent error messages. -[kernel] type_redef.i:31: Failure: - redefinition of a typedef in a non-global scope is currently unsupported -[kernel] type_redef.i:35: User Error: - redefinition of type 'vi' in the same scope with incompatible type. - Previous declaration was at type_redef.i:34 -[kernel] type_redef.i:38: User Error: - redefinition of type 'ci' in the same scope with incompatible type. - Previous declaration was at type_redef.i:37 -[kernel] type_redef.i:41: User Error: - redefinition of type 'ai' in the same scope is only allowed in C11 (option -c11). - Previous declaration was at type_redef.i:40 -[kernel] type_redef.i:44: User Error: - redefinition of type 'ftest_t' in the same scope with incompatible type. - Previous declaration was at type_redef.i:43 -[kernel] type_redef.i:48: User Error: - redefinition of type 'stt' in the same scope is only allowed in C11 (option -c11). - Previous declaration was at type_redef.i:47 -[kernel] type_redef.i:49: User Error: - redefinition of type 'stt' in the same scope with incompatible type. - Previous declaration was at type_redef.i:47 -[kernel:parser:unsupported] type_redef.i:53: Warning: - block-level typedefs currently unsupported; - trying to convert it to a global-level typedef. - Note that this may lead to incoherent error messages. -[kernel] type_redef.i:53: Failure: - redefinition of a typedef in a non-global scope is currently unsupported -[kernel:parser:unsupported] type_redef.i:57: Warning: - block-level typedefs currently unsupported; - trying to convert it to a global-level typedef. - Note that this may lead to incoherent error messages. -[kernel] type_redef.i:57: Failure: - redefinition of a typedef in a non-global scope is currently unsupported -[kernel:parser:unsupported] type_redef.i:62: Warning: - block-level typedefs currently unsupported; - trying to convert it to a global-level typedef. - Note that this may lead to incoherent error messages. -[kernel] type_redef.i:62: Failure: - redefinition of a typedef in a non-global scope is currently unsupported -[kernel:parser:unsupported] type_redef.i:63: Warning: - block-level typedefs currently unsupported; - trying to convert it to a global-level typedef. - Note that this may lead to incoherent error messages. -[kernel] type_redef.i:63: Failure: - redefinition of a typedef in a non-global scope is currently unsupported -[kernel] User Error: stopping on file "type_redef.i" that has errors. -[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/type_redef.1.res.oracle b/tests/syntax/oracle/type_redef.res.oracle similarity index 100% rename from tests/syntax/oracle/type_redef.1.res.oracle rename to tests/syntax/oracle/type_redef.res.oracle diff --git a/tests/value/oracle/anonymous_field.res.oracle b/tests/value/oracle/anonymous_field.res.oracle index 0f6977d1daf35b8031ba19c3a77e7109fdfd152e..e65919e2d36574d5c3d95800a9d46c2ef24f73e5 100644 --- a/tests/value/oracle/anonymous_field.res.oracle +++ b/tests/value/oracle/anonymous_field.res.oracle @@ -1,6 +1,4 @@ [kernel] Parsing anonymous_field.i (no preprocessing) -[kernel] anonymous_field.i:1: Warning: - unnamed fields are a C11 extension (use -c11 to avoid this warning) [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed