Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #77

Closed
Open
Created Mar 22, 2018 by Jens Gerlach@gerlach

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).

Attachments

  • aaa.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking