2021-03-05 02:45 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002360Frama-CPlug-in > clangpublic2018-02-12 12:31
Assigned Tovirgile 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002360: "Here" as predicate label in statement contract causes Segmentation fault
DescriptionRunning "frama-c -wp rotate_cpp.cpp" on the attached program outputs an error message "rotate_cpp.cpp:5:23: expecting a label argument", and then crashes due to a Segmentation fault. The problem disappears when the statement contract in line 5 is changed into an assertion.
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

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