"assigns" in statement contract causes abort or crash
ID0002361: This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002361 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | Sulfur-20171101 | OS | - | OS Version | Ubuntu 17.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "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".