2021-03-01 23:07 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002361Frama-CPlug-in > clangpublic2018-02-12 12:50
Assigned Tovirgile 
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 Files


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
+Issue History