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.
[Frama-Clang] Cannot refer to variables declared within a block in assertions placed just before the closing brace.
- 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: Frama_Clang
- OS name: Ubuntu
- OS version: 18.04.4 LTS
Steps to reproduce the issue
Write an assertion at the end of a block:
int main() {
{
int x = 3;
//@ assert x == 3;
}
return 0;
}Expected behaviour
The file should be processed without errors. When using the WP plugin, a goal for the assertion should be generated.
Actual behaviour
Frama-C reports an unknown identifier error and no goal is generated.
Fix ideas
- The issue does not happen with C files.
- The issue disappears after inserting some code below the assertion, but before the
}. Even a null statement (a single semicolon) is enough.assertion_at_the_end_of_a_block.cpp