expression "b--3" accepted in ACSL (interpreted as "b - -3"), but not in C
ID0002240: This issue was created automatically from Mantis Issue 2240. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002240 | Frama-C | Kernel > ACSL implementation | public | 2016-07-28 | 2016-12-05 |
| Reporter | Jochen | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | xubuntu | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp aaa.c" on the attached program gives no syntax error, and reports 1/1 goals proven, although the right-hand side expression in line 7 is invalid. Uncommenting line 6, which contains the same expression in C, results in a syntax error, as expected.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information