suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
ID0002371: This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002371 | Frama-C | Plug-in > wp | public | 2018-03-22 | 2020-02-17 |
| Reporter | jens | Assigned To | correnson | Resolution | fixed |
| Priority | none | Severity | feature | Reproducibility | always |
| Platform | Sulfur-20171101 | OS | - | OS Version | Ubuntu 17.10 |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | Frama-C 20-Calcium |
Description :
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.
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. #2285).