[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.
- 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
WP should report an error and probably ignore the invalid clause.
WP prints an error message
[wp] Failure: Logic '<invariant name>' undefined)
and then crashes printing a backtrace (aborts due to an internal error).