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 - 2018 MantisBT Team
Powered by Mantis Bugtracker