Frama-Clang crashes on error in contract
ID0002352: This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002352 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | - |
Description :
The 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.