[wp] shall use per-behaviour assigns at call sites
- Frama-C installation mode: Opam
- Frama-C version: 20.0 (Calcium) (as reported by
- 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
The assigns clause of caller can be proved.
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.
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.