Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #81
Closed
Open
Issue created Jun 12, 2014 by mantis-gitlab-migration@mantis-gitlab-migration

Error in coq code generated by wp

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


Id Project Category View Due Date Updated
ID0001806 Frama-C Plug-in > wp public 2014-06-12 2020-02-17
Reporter davyg Assigned To correnson Resolution fixed
Priority normal Severity minor Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version Frama-C 20-Calcium

Description :

There is a typing error with some code generated by wp.

For example this script :

_Bool g() { return 0; }

//@ensures x == (!!\result == !!x); _Bool f(_Bool x) { return g(); }

When using prover coq from wp generates :

Goal forall (f_0 x_0 : Z), ((is_uint32 f_0%Z)) -> ((is_uint32 x_0%Z)) -> ((((Zneq_bool 0 x_0)) = ((Zeq_bool ((Zneq_bool 0 f_0)) ((Zneq_bool 0 x_0)))))%Z)%Z.

Proof. (* auto with zarith. *) Qed.

which produce this coq error on "Zneq_bool 0 f_0":

Error: In environment f_0 : int x_0 : int The term "Zneq_bool 0 f_0" has type "bool" while it is expected to have type "int".

Steps To Reproduce :

Just use the C example with wp/coq as prover (with the gui for example because else wp consider that the script fails and does not print the error)

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