no diagnostics on wrong keyword
ID0002351: This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002351 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | - |
Description :
The attached ACSL/C code contains a typo in the assigns clause: "assign" instead of "assigns".
Frama-Clang provides no diagnostic message on this
frama-c -wp -wp-rte wrong_keyword.cpp [kernel] Parsing wrong_keyword.cpp (external front-end) Now output intermediate result [rte] annotating function foo [wp] 0 goal scheduled [wp] Proved goals: 0 / 0
When processed as a normal C file by Frama-C/WP a more appropriated message is shown
frama-c -wp -wp-rte wrong_keyword.c [kernel] Parsing wrong_keyword.c (with preprocessing) wrong_keyword.c:5:[kernel] user error: unexpected token 'a' [kernel] user error: stopping on file "wrong_keyword.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input.