Frama-C Bug Tracking System - Frama-C
View Issue Details
0002351Frama-CPlug-in > clangpublic2018-01-31 18:052018-01-31 18:06
Frama-C 16-Sulfur 
0002351: no diagnostics on wrong keyword
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.
No tags attached.
cpp wrong_keyword.cpp (55) 2018-01-31 18:05
Issue History
2018-01-31 18:05jensNew Issue
2018-01-31 18:05jensStatusnew => assigned
2018-01-31 18:05jensAssigned To => virgile
2018-01-31 18:05jensFile Added: wrong_keyword.cpp
2018-01-31 18:06jensNote Added: 0006515

2018-01-31 18:06   
might be related to #2348