2020-12-05 00:20 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002371Frama-CPlug-in > wppublic2020-02-17 18:08
Reporterjens 
Assigned Tocorrenson 
PrioritynoneSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002371: suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
DescriptionI ran
"frama-c -wp -wp-out without_lemma -wp-gen -wp-prover why3 -wp-prop=-@lemma aaa.c"
and then
"frama-c -wp -wp-out with_lemma -wp-gen -wp-prover why3 aaa.c"
on the attached file.
After that, "diff -r without_lemma with_lemma" reports no difference between both generated directories.

It is clear that Frama-C needs to generate why3 code for the lemma in both cases, since it might be *used* in some proof.

However, as a consequence, there is no information in the generated directories about which lemmas should be proven. It would be nice if in the long run such information could be provided, e.g. in a separate file.

Additional InformationOur application scenario is the following:

We run (one of) the above command(s) on a local computer to generate why3 files; then we transfer them to a more powerful remote computer, and run the provers there. On the remote computer, we would like to have the list of lemmas-to-be-proven available.

Note that arbitrarily complex combinations of "-wp-prop" could exclude some lemmas from being proven and include others. Therefore, we don't want to perform the evaluation of command-line args "-wp-prop=..." ourselves again (this is difficult, anyway, cf. 0002285).
TagsNo tags attached.
Attached Files
  • c file icon aaa.c (198 bytes) 2018-03-22 12:35 -
    //@ lemma aaa: \forall integer p, q; p>0 && q > 0 ==> p+q>=42;
    
    //@ ensures bbb: \result == 42;
    int foo(int x,int y) {
    	x += 1;
    	//@ assert ccc: x>0;
    	y += 1;
    	//@ assert ddd: y>0;
    	return x+y;
    }
    
    
    c file icon aaa.c (198 bytes) 2018-03-22 12:35 +

-Relationships
+Relationships

-Notes

~0006541

correnson (manager)

Such features will be, indeed, implemented as part of the new generation engine we are working on.
More precisely, we are planning to integrate more closely Frama-C/WP and Why3 session. Hence,
the data (and dependencies) you are asking for will be directly implemented in terms of Why3 tasks.

~0006903

correnson (manager)

New output engine actually uses why3 and generates tasks that are printed in -wp-out directory when provided. Although, you now have a cache of prover results to increase replay performances.

~0006949

signoles (manager)

Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2018-03-22 12:35 Jochen New Issue
2018-03-22 12:35 Jochen Status new => assigned
2018-03-22 12:35 Jochen Assigned To => correnson
2018-03-22 12:35 Jochen File Added: aaa.c
2018-03-22 18:40 virgile Reporter Jochen => jens
2018-03-26 09:39 correnson Note Added: 0006541
2019-10-17 17:10 correnson Note Added: 0006903
2019-10-17 17:11 correnson Status assigned => resolved
2019-10-17 17:11 correnson Fixed in Version => Frama-C 20-Calcium
2019-10-17 17:11 correnson Resolution open => fixed
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006949
+Issue History