The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
[wp] crash when using a type invariant in place of a predicate
- the issue has not yet been reported on Gitlab;
- the issue has not yet been reported on our BTS;
- you installed Frama-C as prescribed in the instructions.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 21.1 (Scandium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 18.04.4 LTS
Steps to reproduce the issue
Define a type invariant and use it in place of a predicate in an expression (in an assertion, an ensures clause, a requires clause, etc.). Run frama-c -wp
Expected behaviour
WP should report an error and probably ignore the invalid clause.
Actual behaviour
WP prints an error message
[wp] Failure: Logic '<invariant name>' undefined)
and then crashes printing a backtrace (aborts due to an internal error).
Fix ideas
None