Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • 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
  • #41

Closed
Open
Created Nov 01, 2020 by Jens Gerlach@gerlach3 of 3 tasks completed3/3 tasks

Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems

I updated the title after figuring out a solution

  • the issue has not yet been reported on Gitlab;
  • the issue has not yet been reported on our BTS;
  • you installed Frama-C as prescribed in the instructions.

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: 22.0-beta (Titanium)
  • Plug-in used: WP
  • OS name: Xubuntu
  • OS version: Ubuntu 20.04.1 LTS

Please add specific information deemed relevant with regard to this issue.

I am able to use the options -wp-prover Alt-Ergo -wp-prover native:coq with ACSL by Example. However when using either -wp-prover Z3 or -wp-prover z3 I receive the following error message. (Note that z3 (4.8.6) has been installed and that it has been successfully registered with why3 config --full-config)

[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals:   25 / 25
  Qed:              16  (2ms-6ms-20ms)
  Alt-Ergo 2.3.3:    9  (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.

Similar with CVC4 and cvc4.

Edited Nov 01, 2020 by Jens Gerlach
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking