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
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
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
(0006515)
jens (reporter)
2018-01-31 18:06

might be related to #2348

- 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