GitLab

• 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

type_invariant_crash.c

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