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.
|ID0002240||Frama-C||Kernel > ACSL implementation||public||2016-07-28||2016-12-05|
|Reporter||Jochen||Assigned To||virgile||Resolution||no change required|
|Product Version||Frama-C Aluminium||Target Version||-||Fixed in Version||-|
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.