[wp] tests to show the bugs

src/plugins/wp/tests/wp_bts/issue_715_a.i

+/*@
+  requires *s >= 0 ;
+*/
+void dummy(int *s);
+
+void foo(void)
+{
+  int p[1] = { 0 };
+  dummy(p);
+}

src/plugins/wp/tests/wp_bts/issue_715_b.i

+//@ predicate isValid(int *s) = \valid(s);
+
+/*@
+  requires isValid(dest);
+  requires dest[0] >= 0;
+*/
+void dummy(int *dest);
+
+void foo(){
+  int p[1] = { 0 } ;
+  dummy(p);
+}

src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_a.i:6: Warning: 
+  No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_a.i, line 2) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_a.i, line 9)
+:
+Assume { Type: is_sint32(p). (* Initializer *) Init: p[0] = 0. }
+Prove: 0 <= p.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_b.i:9: Warning: 
+  No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_b.i, line 4) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_b.i, line 11)
+:
+Assume { (* Heap *) Have: linked(Malloc_0). }
+Prove: P_isValid(Malloc_0, shift_sint32(global(L_p_28), 0)).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_b.i, line 5) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_b.i, line 11)
+:
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_a.i:6: Warning: 
+  No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] Failure: Error in why3:anomaly: File "src/plugins/wp/ProverWhy3.ml", line 586, characters 9-15: Assertion failed
+  Raised at file "src/plugins/wp/ProverWhy3.ml", line 586, characters 9-21
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 383, characters 16-41
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 542, characters 10-33
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 578, characters 10-26
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 575, characters 25-51
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 304, characters 27-53
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 542, characters 10-33
+  Called from file "src/libraries/stdlib/extlib.ml", line 343, characters 14-17
+  Re-raised at file "src/libraries/stdlib/extlib.ml", line 343, characters 41-48
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 963, characters 10-44
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 978, characters 17-57
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 1258, characters 19-34
+  Called from file "src/plugins/wp/wpContext.ml", line 136, characters 17-20
+  Re-raised at file "src/plugins/wp/wpContext.ml", line 141, characters 23-32
+  Called from file "src/plugins/wp/ProverWhy3.ml", line 1255, characters 4-1023
+[kernel] Current source was: tests/wp_bts/issue_715_a.i:6
+  The full backtrace is:
+  Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 532, characters 24-31
+  Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1098, characters 17-55
+  Called from file "src/kernel_services/plugin_entry_points/log.ml", line 525, characters 9-23
+  Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 528, characters 9-16
+  Called from file "src/plugins/wp/prover.ml", line 62, characters 2-34
+  Called from file "src/libraries/utils/task.ml", line 93, characters 38-43
+  Called from file "src/libraries/utils/task.ml", line 93, characters 38-43
+  Called from file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
+  Called from file "src/libraries/utils/task.ml", line 363, characters 14-36
+  Re-raised at file "src/libraries/utils/task.ml", line 369, characters 6-13
+  Called from file "src/libraries/utils/task.ml", line 463, characters 9-22
+  Called from file "array.ml", line 90, characters 31-48
+  Called from file "src/libraries/utils/task.ml", line 480, characters 4-45
+  Called from file "src/libraries/utils/task.ml", line 344, characters 14-18
+  Called from file "src/plugins/wp/register.ml", line 682, characters 4-35
+  Called from file "src/plugins/wp/register.ml", line 768, characters 8-23
+  Called from file "src/libraries/stdlib/extlib.ml", line 343, characters 14-17
+  Re-raised at file "src/libraries/stdlib/extlib.ml", line 343, characters 41-48
+  Called from file "src/libraries/stdlib/extlib.ml", line 344, characters 2-12
+  Called from file "src/libraries/stdlib/extlib.ml", line 344, characters 2-12
+  Called from file "queue.ml", line 105, characters 6-15
+  Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
+  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
+  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
+  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
+  
+  Plug-in wp aborted: internal error.
+  Please report as 'crash' at http://bts.frama-c.com/.
+  Your Frama-C version is 19.0+dev (Potassium).
+  Note that a version and a backtrace alone often do not contain enough
+  information to understand the bug. Guidelines for reporting bugs are at:
+  http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json

+{ "wp:global": { "qed": { "total": 1, "valid": 1 },
+                 "wp:main": { "total": 2, "valid": 1, "unknown": 1 } },
+  "wp:functions": { "foo": { "dummy_requires_2": { "qed": { "total": 1,
+                                                            "valid": 1 },
+                                                   "wp:main": { "total": 1,
+                                                                "valid": 1 } },
+                             "dummy_requires": { "wp:main": { "total": 1,
+                                                              "unknown": 1 } },
+                             "wp:section": { "qed": { "total": 1,
+                                                      "valid": 1 },
+                                             "wp:main": { "total": 2,
+                                                          "valid": 1,
+                                                          "unknown": 1 } } } } }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_b.i:9: Warning: 
+  No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] Warning: creating session directory `tests/wp_bts/oracle_qualif/issue_715_b.0.session'
+[wp] [Failed] Goal typed_foo_call_dummy_requires
+[wp] [Qed] Goal typed_foo_call_dummy_requires_2 : Valid
+[wp] Proved goals:    1 / 2
+  Qed:             1
+[wp] Report in:  'tests/wp_bts/oracle_qualif/issue_715_b.0.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/issue_715_b.0.report.json'
+-------------------------------------------------------------
+Functions           WP     Alt-Ergo        Total   Success
+foo                  1     -                 2      50.0%
+-------------------------------------------------------------