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 0
    • Merge requests 0
  • 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
  • #403

Closed
Open
Created Jun 16, 2016 by Jochen Burghardt@burghardt

workaround for coq-8.5.1 issue?

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


Id Project Category View Due Date Updated
ID0002233 Frama-C Plug-in > wp public 2016-06-16 2016-12-05
Reporter Jochen Assigned To correnson Resolution no change required
Priority none Severity feature Reproducibility always
Platform Aluminium-20160501 OS xubuntu16.04 OS Version -
Product Version - Target Version - Fixed in Version -

Description :

We ran the command

frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.c

on the attached file "adi.c", using the attached Coq-script "wp0.script".

The goal isn't proven, and when manually starting the Coq Ide, it complains:

Error: The reference Q_UnchangedSection was not found in the current

environment.

However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).

For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.

Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.

Attachments

  • adi.c
  • wp0.script
  • Axiomatic.v
  • lemma_AdjacentDifferenceInverse_Coq.v
  • adi.script
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking