Skip to content
GitLab
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 174
    • Issues 174
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • 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
  • #620
Closed
Open
Issue created Dec 28, 2014 by Jens Gerlach@gerlach

unable to use lemma separated_region

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


Id Project Category View Due Date Updated
ID0002041 Frama-C Plug-in > wp public 2014-12-28 2015-06-29
Reporter jens Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

I am using two Frama-C installation:

1.) Neon-20140301 installed through opam under OS X 2.) Neon-20140301+dev-stance manually installed under Linix

In both installations the lemma separated_region in file FRAMAC_SHARE/wp/coqwp/Memory.v is unaccessible because it is put in comments. I suspect that this is the reason why I cannot prove that a local struct variable is separated from one that a function receives as an argument.

What is the reason that this lemma is not available?

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