"Here" as predicate label in statement contract causes Segmentation fault
ID0002360: This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002360 | 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 | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp rotate_cpp.cpp" on the attached program outputs an error message "rotate_cpp.cpp:5:23: expecting a label argument", and then crashes due to a Segmentation fault. The problem disappears when the statement contract in line 5 is changed into an assertion.