From c18e4bc4a76364b20b522b7faf64a36eba6bd58d Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Fri, 11 Sep 2020 18:11:17 +0200 Subject: [PATCH] [kernel] Update tests --- tests/spec/oracle/annot_decl_bts1009.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.0.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.1.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.2.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.3.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.4.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.5.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.6.res.oracle | 2 +- tests/syntax/oracle/cert_msc_38.7.res.oracle | 2 +- tests/syntax/oracle/incomplete_struct_field.res.oracle | 3 ++- tests/syntax/oracle/mutually_recursive_struct.res.oracle | 3 ++- 11 files changed, 13 insertions(+), 11 deletions(-) diff --git a/tests/spec/oracle/annot_decl_bts1009.res.oracle b/tests/spec/oracle/annot_decl_bts1009.res.oracle index bbf8d6510c0..c947f45a80f 100644 --- a/tests/spec/oracle/annot_decl_bts1009.res.oracle +++ b/tests/spec/oracle/annot_decl_bts1009.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/spec/annot_decl_bts1009.i (no preprocessing) -[kernel:annot-error] Warning: +[kernel:annot-error] tests/spec/annot_decl_bts1009.i:5: Warning: Statement contract and ACSL pragmas over a local definition are not implemented. Ignoring annotation /* Generated by Frama-C */ void f(void) diff --git a/tests/syntax/oracle/cert_msc_38.0.res.oracle b/tests/syntax/oracle/cert_msc_38.0.res.oracle index f6f03be6c14..436be5934df 100644 --- a/tests/syntax/oracle/cert_msc_38.0.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.0.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:25: Warning: assert is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] tests/syntax/cert_msc_38.c:25: User Error: Cannot resolve variable assert diff --git a/tests/syntax/oracle/cert_msc_38.1.res.oracle b/tests/syntax/oracle/cert_msc_38.1.res.oracle index 2a38adfac84..912e7c39eda 100644 --- a/tests/syntax/oracle/cert_msc_38.1.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.1.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:32: Warning: Attempt to declare errno as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C [kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information. [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/cert_msc_38.2.res.oracle b/tests/syntax/oracle/cert_msc_38.2.res.oracle index 93f72be060a..9f32d360013 100644 --- a/tests/syntax/oracle/cert_msc_38.2.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.2.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:37: Warning: Attempt to declare math_errhandling as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C [kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information. [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 f85b07111ff..1d21e57a88d 100644 --- a/tests/syntax/oracle/cert_msc_38.3.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.3.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:42: Warning: va_start is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] tests/syntax/cert_msc_38.c:42: User Error: Cannot resolve variable va_start diff --git a/tests/syntax/oracle/cert_msc_38.4.res.oracle b/tests/syntax/oracle/cert_msc_38.4.res.oracle index e8c0de5ba19..a65e4b430e8 100644 --- a/tests/syntax/oracle/cert_msc_38.4.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.4.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:46: Warning: va_copy is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] tests/syntax/cert_msc_38.c:46: User Error: Cannot resolve variable va_copy diff --git a/tests/syntax/oracle/cert_msc_38.5.res.oracle b/tests/syntax/oracle/cert_msc_38.5.res.oracle index 7d12efef567..38293bc7042 100644 --- a/tests/syntax/oracle/cert_msc_38.5.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.5.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:50: Warning: va_arg is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] tests/syntax/cert_msc_38.c:50: User Error: Cannot resolve variable va_arg diff --git a/tests/syntax/oracle/cert_msc_38.6.res.oracle b/tests/syntax/oracle/cert_msc_38.6.res.oracle index cbd86b6a84b..5aad28f718a 100644 --- a/tests/syntax/oracle/cert_msc_38.6.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.6.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:54: Warning: va_end is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] tests/syntax/cert_msc_38.c:54: User Error: Cannot resolve variable va_end diff --git a/tests/syntax/oracle/cert_msc_38.7.res.oracle b/tests/syntax/oracle/cert_msc_38.7.res.oracle index 6db601e9319..a13d4f25031 100644 --- a/tests/syntax/oracle/cert_msc_38.7.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.7.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing) -[kernel:CERT:MSC:38] Warning: +[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:59: Warning: setjmp is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information. [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 d75500699ee..1da6f42644d 100644 --- a/tests/syntax/oracle/incomplete_struct_field.res.oracle +++ b/tests/syntax/oracle/incomplete_struct_field.res.oracle @@ -3,6 +3,7 @@ declaration of array of incomplete type 'struct _s` [kernel] tests/syntax/incomplete_struct_field.i:1: User Error: field `v' is declared with incomplete type struct _s [12] -[kernel] User Error: type struct _s is circular +[kernel] tests/syntax/incomplete_struct_field.i:1: User Error: + type struct _s is circular [kernel] User Error: stopping on file "tests/syntax/incomplete_struct_field.i" that has errors. [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 56467d6859b..74ebf746db9 100644 --- a/tests/syntax/oracle/mutually_recursive_struct.res.oracle +++ b/tests/syntax/oracle/mutually_recursive_struct.res.oracle @@ -7,6 +7,7 @@ declaration of array of incomplete type 'struct S1` [kernel] tests/syntax/mutually_recursive_struct.i:6: User Error: field `s1' is declared with incomplete type struct S1 [2] -[kernel] User Error: type struct S2 is circular +[kernel] tests/syntax/mutually_recursive_struct.i:6: User Error: + type struct S2 is circular [kernel] User Error: stopping on file "tests/syntax/mutually_recursive_struct.i" that has errors. [kernel] Frama-C aborted: invalid user input. -- GitLab