Frama-C Bug Tracking System - Frama-C
View Issue Details
0002351Frama-CPlug-in > clangpublic2018-01-31 18:052018-01-31 18:06
jens 
virgile 
normalminoralways
assignedopen 
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
https://bts.frama-c.com/file_download.php?file_id=1235&type=bug
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

Notes
(0006515)
jens   
2018-01-31 18:06   
might be related to 0002348