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). ## Attachments - [aaa.c](/uploads/ef6c959b3687621110ddcbd77ab2b906/aaa.c)