Frama-C Bug Tracking System - Frama-C
View Issue Details
0002336Frama-CPlug-in > wppublic2017-12-08 12:522019-10-17 18:02
Jochen 
correnson 
normaltweakalways
closedsuspended 
Sulfur-20171101Ubuntu 17.04
 
 
0002336: suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
Running "frama-c -wp -wp-rte foo.c -wp-out wp-out" on the attached file fails to prove clauses "E1" (as expected) and "E2". The latter is provable from "E1" by axiom "a2". A look at file "main_post_E2_Alt-Ergo.mlw" reveals that "E1" isn't given as hypothesis, and hence axiom "a2" can't be applied. I cannot judge whether there is good reason for this behavior of Frama-C/Wp. If there isn't, I suggest that "E1" should be given as hypothesis to the proof obligation for "E2", similar to Frama-C/Wp's behavior on consecutive "assigns" clauses. The same applies to statement contracts.
No tags attached.
c foo.c (247) 2017-12-08 12:52
https://bts.frama-c.com/file_download.php?file_id=1215&type=bug
Issue History
2017-12-08 12:52JochenNew Issue
2017-12-08 12:52JochenStatusnew => assigned
2017-12-08 12:52JochenAssigned To => correnson
2017-12-08 12:52JochenFile Added: foo.c
2017-12-08 12:54JochenNote Added: 0006481
2019-10-17 17:21corrensonNote Added: 0006908
2019-10-17 17:22corrensonStatusassigned => resolved
2019-10-17 17:22corrensonResolutionopen => suspended
2019-10-17 18:02signolesStatusresolved => closed

Notes
(0006481)
Jochen   
2017-12-08 12:54   
In fact, I observed the problem when I tried to prove an "ensures" from a statement contract, and inserted an easier-to-prove clause as another "ensures" before it. The suggested change would make this method work.
(0006908)
correnson   
2019-10-17 17:21   
This is an interesting option. We shall try to investigate it.