From d0ece096a67f28a7f51488526818a5513f113715 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Tue, 31 Jan 2023 16:40:53 +0100 Subject: [PATCH] [wp] update tests oracles --- 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 - 12 files changed, 14 deletions(-) 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 34f2dbbb29f..aaf2d71df37 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 94270ebda6c..66813c9d2fe 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 cd5f472d890..cd18f6c56b2 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 e8646eaade5..02b2ed5961d 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 216d2d5f059..1e559e3b03e 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 e0639cf9443..78ddf615c38 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 86e36652590..8acd7a5746f 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 d4bf8877faf..071c3882ef8 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 d96825e3224..b76958430dd 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 bf4fa14f4c9..48504f84e84 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 0a16f67da1a..fbc663bb95a 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 7013f6d336b..63bddb63b6a 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[]) -- GitLab