Function with name shift produces error
ID0001265: This issue was created automatically from Mantis Issue 1265. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001265 | Frama-C | Plug-in > jessie | public | 2012-08-08 | 2013-03-27 |
| Reporter | boris | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
The function
void shift() {}
gives rise to the the message
File "why/car.why", line 282, characters 10-15: Clash with previous constant shift make: *** [car.stat] Error 1 [jessie] user error: Jessie subprocess failed: make -f car.makefile gui
Renaming shift() avoids the problem.
why version 2.31, command line: frama-c -jessie -jessie-atp=gui -pp-annot