[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
Edited by Jakub Szabelewski