| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002352 | Frama-C | Plug-in > clang | public | 2018-01-31 18:17 | 2018-01-31 18:17 |
|
| Reporter | jens | |
| Assigned To | virgile | |
| Priority | normal | Severity | crash | Reproducibility | always |
| Status | assigned | Resolution | open | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C 16-Sulfur | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0002352: Frama-Clang crashes on error in contract |
| 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.
|
| Tags | No tags attached. |
|
| Attached Files |  assignment_in_contract.cpp [^] (73 bytes) 2018-01-31 18:17 |
|
Relationships 
Relationships