Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002361Frama-CPlug-in > clangpublic2018-02-12 12:502018-02-12 12:50
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product Version 
Target VersionFixed in Version 
Summary0002361: "assigns" in statement contract causes abort or crash
DescriptionRunning "frama-c remove_cpp.cpp" on the attached program outputs

"framaCIRGen: ACSLStatementAnnotation.cpp:248: Parser::Base::ReadResult Acsl::StatementAnnotation::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed."

and then aborts. If the "ensures" clause in line 5 is removed, Frama-C outputs instead:

"*** Error in `framaCIRGen': double free or corruption (out): 0x0000559f983d0160 ***"

and then aborts, too. If in addition "a[0..9]" is removed from the "assigns" claus in line 4, Frama-C crashes (Segmentation fault) without printing any error message before. For the latter reason, I've set the severity to "crash".
TagsNo tags attached.
Attached Filescpp file icon remove_cpp.cpp [^] (132 bytes) 2018-02-12 12:50

- Relationships

-  Notes
There are no notes attached to this issue.

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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker