Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002360Frama-CPlug-in > clangpublic2018-02-12 12:312018-02-12 12:31
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
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 Filescpp file icon rotate_cpp.cpp [^] (102 bytes) 2018-02-12 12:31

- Relationships

-  Notes
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker