Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002352Frama-CPlug-in > clangpublic2018-01-31 18:172018-01-31 18:17
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002352: Frama-Clang crashes on error in contract
DescriptionThe attached example uses mistakenly the assignment operator = instead of == in the ensures clause. Frama-Clang crashes on this example. frama-c -wp -wp-rte assignment_in_contract.cpp [kernel] Parsing assignment_in_contract.cpp (external front-end) framaCIRGen: ACSLTermOrPredicate.cpp:7096: Parser::Base::ReadResult Acsl::TermOrPredicate::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed. Aborted (core dumped) [kernel] user error: Failed to parse C++ file. See Clang messages for more information [kernel] user error: stopping on file "assignment_in_contract.cpp" that has errors. [kernel] Frama-C aborted: invalid user input. A message along the lines of normal Frama-C "user error: Assignment operators not allowed in annotations." would be more helpful.
TagsNo tags attached.
Attached Filescpp file icon assignment_in_contract.cpp [^] (73 bytes) 2018-01-31 18:17

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2018-01-31 18:17 jens New Issue
2018-01-31 18:17 jens Status new => assigned
2018-01-31 18:17 jens Assigned To => virgile
2018-01-31 18:17 jens File Added: assignment_in_contract.cpp


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker