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
  • #102

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

alt-ergo support in Frama-C 20 beta

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


Id Project Category View Due Date Updated
ID0002484 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 :

This is a hint to (better) describe the transition from using alt-ergo in Frama-C 19 and 20. If it is already described, then I apologize.

In Frama-C 19 and before one uses
-wp-prover alt-ergo for the native interface and -wp-prover why3:alt-ergo for the Why3 interface

In Frama-C 20 the respective options are -wp-prover native:alt-ergo for the native interface and -wp-prover alt-ergo

I propose that it is described with other things in a short transition document.

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#102