2021-03-01 22:57 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002359Frama-CPlug-in > clangpublic2018-02-12 10:49
Assigned Tovirgile 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002359: Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't
DescriptionRunning "frama-c -wp st.cpp" on the attached program produces a (stderr) message "st.cpp:2:14: keyword 'keyword -> invariant' encountered when parsing term or predicate". When 'invariant' is changed e.g. to 'assert', a similar message is printed.

When the file is renamed to "st.c", the message disappears. Likewise, our use of a reserved keyword as procedure or parameter name didn't cause such a message.
TagsNo tags attached.
Attached Files
  • cpp file icon st.cpp (59 bytes) 2018-02-12 10:49


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2018-02-12 10:49 Jochen New Issue
2018-02-12 10:49 Jochen Status new => assigned
2018-02-12 10:49 Jochen Assigned To => virgile
2018-02-12 10:49 Jochen File Added: st.cpp
+Issue History