Frama-C Bug Tracking System - Frama-C
View Issue Details
0001469Frama-CKernelpublic2013-08-21 17:312014-03-13 15:57
pascal 
virgile 
normalmajoralways
closedfixed 
 
Frama-C Neon-20140301 
0001469: Unsound transformation of ACSL annotations
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.
No tags attached.
Issue History
2013-08-21 17:31pascalNew Issue
2013-08-21 17:32pascalDescription Updated
2013-08-21 17:33pascalStatusnew => assigned
2013-08-21 17:33pascalAssigned To => virgile
2013-09-02 15:58svnCheckin
2013-09-02 15:58svnStatusassigned => resolved
2013-09-02 15:58svnResolutionopen => fixed
2014-02-12 16:57Note Added: 0004561
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004561)
   
2014-02-12 16:57   
Fix committed to stable/neon branch.