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 aaf2d71df37874351849fd00cad82103468c01c0..34f2dbbb29f7a37903e3d9d3754f8beb51181eb2 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 66813c9d2fe911d3e4acfed55c4940dfa1bacbcd..94270ebda6c0aa5f2c4be821aa1d095f02cfe896 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 cd18f6c56b26e52516835bb0641f54a29a682bd4..cd5f472d8907f518524840aea815f0ac4f190880 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 02b2ed5961d8d48a38256c0d9b1e01304db00714..e8646eaade5996391129c595f60c0738c1a8f67d 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 1e559e3b03e10e2526958651c62444c5788e5e0a..216d2d5f059baf070a26f4f2c0b07780316af32b 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 78ddf615c388fbb450e6f01f9deb175c6107177b..e0639cf944315438d96fa0f096c23b1d31a64771 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 8acd7a5746f35c5aaa87e61f545d317a55814df3..86e366525909ee143dbcd0cf4445e246d5b86682 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 071c3882ef864c99746b31c65f61d79bd3750fe8..d4bf8877fafc2c7eb40afc4ba81b0e6445947870 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 b76958430dd6ad124abc0dd2d3c95115c54b2153..d96825e3224545beb5f24098f0eb80ea4f0a718f 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 48504f84e84b76225c3d8a3900a5e24c716dddf2..bf4fa14f4c96fe42234c2157be97278f47194bbd 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 fbc663bb95acbeac2fcb60827b93d357b57d006a..0a16f67da1a01313b9c9ec98e0229a527145d21d 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 63bddb63b6a6d0163cb7c835238023a22a0ebfb0..7013f6d336b811ff02cc70566fa29da9fdea1cc0 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 664328c9384b362461687bb897d248ad07b40d80..e0ab0227317fc5ff78b8e843dfb0c1a504ba2659 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 c65343692b545464ab010a6e10926ed10f81c934..cbc565cc0f40018955b84c7012397b9ed9a49b10 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