unknown variable in contract is not treated as an error
ID0002348: This issue was created automatically from Mantis Issue 2348. Further discussion may take place here.
|ID0002348||Frama-C||Plug-in > clang||public||2018-01-30||2018-01-30|
|Product Version||-||Target Version||-||Fixed in Version||-|
The attached C/C++ code is treated differently by Frama-C and Frama-Clang The C file 'unknown_variable.c' is correctly rejected by Frama-C with wit the the message
frama-c -wp -wp-rte unknown_variable.c
[kernel] user error: stopping on file "unknown_variable.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command.
When processing this file as C++ code
frama-c -wp -wp-rte unknown_variable.cpp
Frama-Clang only emits a warning (by the kernel) and continues processing
Parsing unknown_variable.cpp (external front-end) unknown_variable.cpp:6:18: unknown identifier 'c' Now output intermediate result
In my opinion, the C++ contract should be rejected as well.