diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i index ccde8d32cf69e67cc1595503336e8a461d1b98aa..b0caa16f3bfe247292a9c873c9ad259a5ef65237 100644 --- a/src/plugins/wp/tests/wp_plugin/dynamic.i +++ b/src/plugins/wp/tests/wp_plugin/dynamic.i @@ -61,7 +61,7 @@ int h0(void); @ assigns X1; @ ensures X1==1; */ int behavior (int (*p)(void)) { - //@ calls h1, h2; // Shall not be proved in default behavior (known bug) + //@ calls h1, h2; // Shall not be proved in default behavior return (*p)(); } diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle index ad37a67830bf85dd03dd6f3a058108f367ee9ea3..ef17fe7f5adf94799c6156601656f481b363fec2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle @@ -10,8 +10,17 @@ [wp] tests/wp_plugin/dynamic.i:87: Calls h1 [wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g [wp:calls] Dynamic call(s): 6. -[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior [wp] Warning: Missing RTE guards +[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior +------------------------------------------------------------ + Function behavior +------------------------------------------------------------ + +Goal Call point h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65): +Assume { (* Heap *) Type: region(p.base) <= 0. } +Prove: (global(G_h1_61) = p) \/ (global(G_h2_67) = p). + +------------------------------------------------------------ ------------------------------------------------------------ Function behavior with behavior bhv1 ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle index e3e408c44c11240b3f222cc20901d0fcf6b2d977..544241057280ba7e544a974feefee52e98871e9c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle @@ -13,6 +13,7 @@ [wp] [Qed] Goal typed_guarded_call_ensures_part2 : Valid [wp] [Qed] Goal typed_guarded_call_ensures_2_part1 : Valid [wp] [Qed] Goal typed_guarded_call_ensures_2_part2 : Valid +[wp] [Alt-Ergo] Goal typed_behavior_call_point_h1_h2_s15 : Unsuccess [wp] [Qed] Goal typed_behavior_call_point_h1_h2_s15 : Valid [wp] [Qed] Goal typed_behavior_bhv1_ensures_part1 : Valid [wp] [Qed] Goal typed_behavior_bhv1_ensures_part2 : Valid