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

Closed
Open
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