Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002351Frama-CPlug-in > clangpublic2018-01-31 18:052018-01-31 18:06
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002351: no diagnostics on wrong keyword
DescriptionThe 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.

TagsNo tags attached.
Attached Filescpp file icon wrong_keyword.cpp [^] (55 bytes) 2018-01-31 18:05

- Relationships

-  Notes
jens (reporter)
2018-01-31 18:06

might be related to 0002348

- Issue History
Date Modified Username Field Change
2018-01-31 18:05 jens New Issue
2018-01-31 18:05 jens Status new => assigned
2018-01-31 18:05 jens Assigned To => virgile
2018-01-31 18:05 jens File Added: wrong_keyword.cpp
2018-01-31 18:06 jens Note Added: 0006515

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker