|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002371||Frama-C||Plug-in > wp||public||2018-03-22 12:35||2020-02-17 18:08|
|Platform||Sulfur-20171101||OS||OS Version||Ubuntu 17.10|
|Product Version||Frama-C 16-Sulfur|
|Target Version||Fixed in Version||Frama-C 20-Calcium|
|Summary||0002371: suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory|
|Description||I ran |
"frama-c -wp -wp-out without_lemma -wp-gen -wp-prover why3 -wp-prop=-@lemma aaa.c"
"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 Information||Our 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).
|Tags||No tags attached.|
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.
|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.|
|Fixed in Frama-C 20.0 (Calcium).|
|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|