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 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & 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
  • #3
Closed
Open
Created May 07, 2020 by Nikolai Kosmatov@nkosmatovDeveloper

[wp] shall use per-behaviour assigns at call sites

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: 20.0 (Calcium) (as reported by frama-c -version)
  • Plug-in used: WP
  • OS name: Ubuntu
  • OS version: 19.10

Please add specific information deemed relevant with regard to this issue.

Steps to reproduce the issue

frama-c-gui -wp behavior_assigns.c

Please indicate here steps to follow which reproduce the issue.

See the attached file for a minimal example. behavior_assigns.c

Expected behaviour

The assigns clause of caller can be proved.

Actual behaviour

The assigns clause of caller is not proved.

The assigns clauses specific for particular behaviors in a callee cannot be used in the caller under specific conditions falling into such behavior(s) to prove a more restrictive assigns clause in the caller, rather than the most general assigns taking into account all behaviors of the callee.

Fix ideas

Obvious workarounds include additional postconditions, that make the specifications more complex and make the proof with WP less powerful. Matching the callee's behaviors to prove stronger assigns clauses in the caller could be helpful.

Edited May 12, 2020 by Loïc Correnson
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking