2021-01-25 14:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002336Frama-CPlug-in > wppublic2019-10-17 18:02
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionsuspended 
PlatformSulfur-20171101OSOS VersionUbuntu 17.04
Product Version 
Target VersionFixed in Version 
Summary0002336: suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
DescriptionRunning "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.
TagsNo tags attached.
Attached Files
  • c file icon foo.c (247 bytes) 2017-12-08 12:52 -
    /*@ 
    	axiomatic a1 {
    		predicate foo(integer x);
    		predicate bar(integer x);
    		axiom a2: \forall integer x; foo(x) ==> bar(x);
    	}
    */
    
    
    /*@
    	assigns \nothing;
    	ensures E1: foo(\result);
    	ensures E2: bar(\result);
    */
    int main(void) {
    	return 1;
    }
    
    
    c file icon foo.c (247 bytes) 2017-12-08 12:52 +

-Relationships
+Relationships

-Notes

~0006481

Jochen (reporter)

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 (manager)

This is an interesting option.
We shall try to investigate it.
+Notes

-Issue History
Date Modified Username Field Change
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
+Issue History