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)
- mitigation: see option
-
WP does not use per behavior assigns
- pub/frama-c#2104
- #3 (closed)
- #1019 (closed)
Suggestions:
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information