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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002348 | Frama-C | Plug-in > clang | public | 2018-01-30 | 2018-01-30 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.