| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001469 | Frama-C | Kernel | public | 2013-08-21 17:31 | 2014-03-13 15:57 |
|
| Reporter | pascal | |
| Assigned To | virgile | |
| Priority | normal | Severity | major | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | Frama-C Neon-20140301 | |
|
| Summary | 0001469: Unsound transformation of ACSL annotations |
| 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. |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships