[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.