Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002348 | Frama-C | Plug-in > clang | public | 2018-01-30 16:31 | 2018-01-30 18:03 |
|
| Reporter | jens | |
| Assigned To | virgile | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | assigned | Resolution | open | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0002348: unknown variable in contract is not treated as an error |
| 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.
|
| Steps To Reproduce | |
| Additional Information | |
| Tags | No tags attached. |
| Relationships | |
| Attached Files |  unknown_variable.c (88) 2018-01-30 16:31
https://bts.frama-c.com/file_download.php?file_id=1230&type=bug
unknown_variable.cpp (88) 2018-01-30 16:31
https://bts.frama-c.com/file_download.php?file_id=1231&type=bug |
|
| Issue History |
| Date Modified | Username | Field | Change |
| 2018-01-30 16:31 | jens | New Issue | |
| 2018-01-30 16:31 | jens | Status | new => assigned |
| 2018-01-30 16:31 | jens | Assigned To | => virgile |
| 2018-01-30 16:31 | jens | File Added: unknown_variable.c | |
| 2018-01-30 16:31 | jens | File Added: unknown_variable.cpp | |
| 2018-01-30 18:03 | virgile | Note Added: 0006512 | |