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

Closed
Open
Created Aug 05, 2021 by Allan Blanchard@blanchardMaintainer0 of 2 tasks completed0/2 tasks

Known WP limitations on `assigns` handling

This issue lists known WP issues with the handling of assigns annotation. Related issues are closed (as duplicates) and listed here.

  • WP assigns verification is stronger than what ACSL specifies
    • mitigation: see option -wp-unfold-assigns
    • #1018 (closed)
    • #1002 (closed)
    • #2584 (closed)
  • WP does not use per behavior assigns
    • pub/frama-c#2104
    • #3 (closed)
    • #1019 (closed)

Suggestions:

  • #337 (closed)
Edited Nov 23, 2021 by Allan Blanchard
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking