2020-12-05 00:20 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002371Frama-CPlug-in > wppublic2020-02-17 18:08
Assigned Tocorrenson 
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 +




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.


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.


signoles (manager)

Fixed in Frama-C 20.0 (Calcium).

-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