Unsound transformation of ACSL annotations
ID0001469: This issue was created automatically from Mantis Issue 1469. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001469 | Frama-C | Kernel | public | 2013-08-21 | 2014-03-13 |
| Reporter | pascal | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
Test in SVN 23392: tests/misc/logic_ptr_cast.i
Obtained result:
[value] Called Frama_C_show_each({{ &t + {0; 4; 8; 12; 16; 20; 24; 28} }}) ... /*@ assert ((((((p == (int *)t || p == (int *)(&t[1])) || p == (int *)(&t[2])) || p == (int *)(&t[3])) || p == (int *)(&t[4])) || p == (int *)(&t[5])) || p == (int *)(&t[6])) || p == (int *)(&t[7]); */
Expected result:
[value] Called Frama_C_show_each({{ &t + {0; 1; 2; 3; 4; 5; 6; 7} }})
and the same assert as the one written in the program.