From 0f4ee44bf1832f844e291d36601108e73f760cfa Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Mon, 30 Jan 2023 16:59:09 +0100 Subject: [PATCH] [tests] update oracles for ill-formed tests with anonymous typedef --- src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle | 2 ++ .../wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle | 2 ++ src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle | 1 + src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle | 1 + src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle | 1 + src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle | 1 + .../wp/tests/wp_plugin/oracle_qualif/dynamic.0.res.oracle | 1 + .../wp/tests/wp_plugin/oracle_qualif/dynamic.1.res.oracle | 1 + src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle | 1 + src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle | 1 + src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle | 1 + src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle | 1 + tests/syntax/oracle/enum_call.res.oracle | 1 + tests/value/oracle/enum.res.oracle | 1 + 14 files changed, 16 insertions(+) diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle index aaf2d71df37..34f2dbbb29f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle @@ -1,5 +1,7 @@ # frama-c -wp [...] [kernel] Parsing assigns_path.i (no preprocessing) +[kernel:parser:unnamed-typedef] assigns_path.i:1: Warning: + typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle index 66813c9d2fe..94270ebda6c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle @@ -1,5 +1,7 @@ # frama-c -wp [...] [kernel] Parsing assigns_path.i (no preprocessing) +[kernel:parser:unnamed-typedef] assigns_path.i:1: Warning: + typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 9 goals scheduled diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle index cd18f6c56b2..cd5f472d890 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp [...] [kernel] Parsing bts_2079.i (no preprocessing) +[kernel:parser:unnamed-typedef] bts_2079.i:7: Warning: typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle index 02b2ed5961d..e8646eaade5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp [...] [kernel] Parsing bts_2079.i (no preprocessing) +[kernel:parser:unnamed-typedef] bts_2079.i:7: Warning: typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle index 1e559e3b03e..216d2d5f059 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp [...] [kernel] Parsing dynamic.i (no preprocessing) +[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name [wp] Running WP plugin... [kernel:dyncalls] Computing dynamic calls. [kernel:dyncalls] dynamic.i:32: Calls f1 f2 diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle index 78ddf615c38..e0639cf9443 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp -wp-no-let [...] [kernel] Parsing dynamic.i (no preprocessing) +[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name [wp] Running WP plugin... [kernel:dyncalls] Computing dynamic calls. [kernel:dyncalls] dynamic.i:32: Calls f1 f2 diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.0.res.oracle index 8acd7a5746f..86e36652590 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.0.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp [...] [kernel] Parsing dynamic.i (no preprocessing) +[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] dynamic.i:80: Warning: Missing 'calls' for default behavior diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.1.res.oracle index 071c3882ef8..d4bf8877faf 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.1.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp -wp-no-let [...] [kernel] Parsing dynamic.i (no preprocessing) +[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 5 goals scheduled diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle index b76958430dd..d96825e3224 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp [...] [kernel] Parsing caveat.i (no preprocessing) +[kernel:parser:unnamed-typedef] caveat.i:10: Warning: typedef without a name [kernel] caveat.i:41: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle index 48504f84e84..bf4fa14f4c9 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing caveat.i (no preprocessing) +[kernel:parser:unnamed-typedef] caveat.i:10: Warning: typedef without a name [kernel] caveat.i:41: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle index fbc663bb95a..0a16f67da1a 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing caveat2.i (no preprocessing) +[kernel:parser:unnamed-typedef] caveat2.i:9: Warning: typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] caveat2.i:14: Warning: Undefined array-size (sint32[]) diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle index 63bddb63b6a..7013f6d336b 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle @@ -1,5 +1,6 @@ # frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing caveat2.i (no preprocessing) +[kernel:parser:unnamed-typedef] caveat2.i:9: Warning: typedef without a name [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] caveat2.i:14: Warning: Undefined array-size (sint32[]) diff --git a/tests/syntax/oracle/enum_call.res.oracle b/tests/syntax/oracle/enum_call.res.oracle index 664328c9384..e0ab0227317 100644 --- a/tests/syntax/oracle/enum_call.res.oracle +++ b/tests/syntax/oracle/enum_call.res.oracle @@ -1,4 +1,5 @@ [kernel] Parsing enum_call.i (no preprocessing) +[kernel:parser:unnamed-typedef] enum_call.i:1: Warning: typedef without a name /* Generated by Frama-C */ enum E { C0 = 0, diff --git a/tests/value/oracle/enum.res.oracle b/tests/value/oracle/enum.res.oracle index c65343692b5..cbc565cc0f4 100644 --- a/tests/value/oracle/enum.res.oracle +++ b/tests/value/oracle/enum.res.oracle @@ -1,4 +1,5 @@ [kernel] Parsing enum.i (no preprocessing) +[kernel:parser:unnamed-typedef] enum.i:5: Warning: typedef without a name [eva] Analyzing a complete application starting at f [eva] Computing initial state [eva] Initial state computed -- GitLab