Wrong WP computation when calling a function with behaviors (assigns problem ?)
ID0000992: This issue was created automatically from Mantis Issue 992. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000992 | Frama-C | Plug-in > wp | public | 2011-10-20 | 2013-04-19 |
| Reporter | Anne | Assigned To | correnson | Resolution | fixed |
| Priority | high | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
Description :
The assert [0==1] is proved Valid in the enclosed example. This is because the proof obligation has an hypothesis [b = b + 1] instead of [b = b' + 1].
This problem appears from rev 15799 which is about [assigns] : [WP] Warning for missing assigns clauses + better merge of assigns for function calls
Additional Information :
$ frama-c toto.c -wp -wp-prop F -wp-print -wp-no-simpl
Proof Obligation assert_1_F: Prover Alt-Ergo returns Valid Environment: Store_env1
- Assumes Post-condition for 'end' (file toto.c, line 10) of 'add'
- Assumes Post-condition for 'ok' (file toto.c, line 6) of 'add'
- Proves Assertion 'F' (file toto.c, line 19) Goal store_f_assert_1_F: let bound_0 = 0 in let bound_1 = bound_0 in ((1000 <= bound_1) -> false) -> ((bound_1 < 1000) -> (bound_0 = (bound_1+1))) -> tag_F:(0 = 1)