|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002336||Frama-C||Plug-in > wp||public||2017-12-08 12:52||2019-10-17 18:02|
|Platform||Sulfur-20171101||OS||OS Version||Ubuntu 17.04|
|Target Version||Fixed in Version|
|Summary||0002336: suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"|
|Description||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.
|Tags||No tags attached.|
|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.|
This is an interesting option.
We shall try to investigate it.
|2017-12-08 12:52||Jochen||New Issue|
|2017-12-08 12:52||Jochen||Status||new => assigned|
|2017-12-08 12:52||Jochen||Assigned To||=> correnson|
|2017-12-08 12:52||Jochen||File Added: foo.c|
|2017-12-08 12:54||Jochen||Note Added: 0006481|
|2019-10-17 17:21||correnson||Note Added: 0006908|
|2019-10-17 17:22||correnson||Status||assigned => resolved|
|2019-10-17 17:22||correnson||Resolution||open => suspended|
|2019-10-17 18:02||signoles||Status||resolved => closed|