Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
F
frama-c
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 202
    • Issues 202
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #101

Closed
Open
Opened Nov 08, 2019 by Jens Gerlach@gerlach

-wp-out missing output for Why3 provers in Frama-C 20 beta

ID0002485: This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002485 Frama-C Plug-in > wp public 2019-11-08 2019-11-08
Reporter jens Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility have not tried
Platform Linux OS xubuntu OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version -

Description :

When the attached programme is processed with

frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c

then the output directory 'abs.wp/typed' contains three files

 abs_ensures_3_Alt-Ergo.mlw
 abs_ensures_3_Alt-Ergo.out
 abs_ensures_3.ergo

When using the command line

frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c

then the output directory 'abs.wp/typed' contains only the generated proof obligation

abs_ensures_3_Why3_Alt_Ergo_2_3_0.why

(similiarly when using another Why3 prover, such as cvc4)

Is there a way to output also the result for Why3 provers?

Attachments

  • abs.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: pub/frama-c#101