diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle index cb8dc37d91b9d30c6484d28f01b8da947626d701..65a87c92522e55733522c0af3f53df5f0ad1680f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle @@ -1,13 +1,7 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing) [wp] Running WP plugin... -[wp] tests/wp_acsl/generalized_checks.i:68: Warning: - Unsupported generalized invariant, use loop invariant instead. - Ignored invariant - check invariant \true; [wp] Warning: Missing RTE guards -[wp] tests/wp_acsl/generalized_checks.i:75: Warning: - Missing assigns clause (assigns 'everything' instead) ------------------------------------------------------------ Axiomatic 'Th' ------------------------------------------------------------