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 34f2dbbb29f7a37903e3d9d3754f8beb51181eb2..aaf2d71df37874351849fd00cad82103468c01c0 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,7 +1,5 @@ # 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 94270ebda6c0aa5f2c4be821aa1d095f02cfe896..66813c9d2fe911d3e4acfed55c4940dfa1bacbcd 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,7 +1,5 @@ # 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 cd5f472d8907f518524840aea815f0ac4f190880..cd18f6c56b26e52516835bb0641f54a29a682bd4 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,6 +1,5 @@ # 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 e8646eaade5996391129c595f60c0738c1a8f67d..02b2ed5961d8d48a38256c0d9b1e01304db00714 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,6 +1,5 @@ # 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 216d2d5f059baf070a26f4f2c0b07780316af32b..1e559e3b03e10e2526958651c62444c5788e5e0a 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,6 +1,5 @@ # 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 e0639cf944315438d96fa0f096c23b1d31a64771..78ddf615c388fbb450e6f01f9deb175c6107177b 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,6 +1,5 @@ # 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 86e366525909ee143dbcd0cf4445e246d5b86682..8acd7a5746f35c5aaa87e61f545d317a55814df3 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,6 +1,5 @@ # 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 d4bf8877fafc2c7eb40afc4ba81b0e6445947870..071c3882ef864c99746b31c65f61d79bd3750fe8 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,6 +1,5 @@ # 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 d96825e3224545beb5f24098f0eb80ea4f0a718f..b76958430dd6ad124abc0dd2d3c95115c54b2153 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,6 +1,5 @@ # 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 bf4fa14f4c96fe42234c2157be97278f47194bbd..48504f84e84b76225c3d8a3900a5e24c716dddf2 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,6 +1,5 @@ # 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 0a16f67da1a01313b9c9ec98e0229a527145d21d..fbc663bb95acbeac2fcb60827b93d357b57d006a 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle @@ -1,6 +1,5 @@ # 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 7013f6d336b811ff02cc70566fa29da9fdea1cc0..63bddb63b6a6d0163cb7c835238023a22a0ebfb0 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,6 +1,5 @@ # 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[])