Frama-C Bug Tracking System - Frama-C
View Issue Details
0002371Frama-CPlug-in > wppublic2018-03-22 12:352019-10-17 17:11
jens 
correnson 
nonefeaturealways
resolvedfixed 
Sulfur-20171101Ubuntu 17.10
Frama-C 16-Sulfur 
Frama-C 20-Calcium 
0002371: suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
I 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.
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. #2285).
No tags attached.
c aaa.c (198) 2018-03-22 12:35
https://bts.frama-c.com/file_download.php?file_id=1257&type=bug
Issue History
2018-03-22 12:35JochenNew Issue
2018-03-22 12:35JochenStatusnew => assigned
2018-03-22 12:35JochenAssigned To => correnson
2018-03-22 12:35JochenFile Added: aaa.c
2018-03-22 18:40virgileReporterJochen => jens
2018-03-26 09:39corrensonNote Added: 0006541
2019-10-17 17:10corrensonNote Added: 0006903
2019-10-17 17:11corrensonStatusassigned => resolved
2019-10-17 17:11corrensonFixed in Version => Frama-C 20-Calcium
2019-10-17 17:11corrensonResolutionopen => fixed

Notes
(0006541)
correnson   
2018-03-26 09:39   
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   
2019-10-17 17:10   
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.