View Issue Details [ Jump to Notes ] | [ 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 | ||||||
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 |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-08-21 17:31 | pascal | New Issue | |
2013-08-21 17:32 | pascal | Description Updated | |
2013-08-21 17:33 | pascal | Status | new => assigned |
2013-08-21 17:33 | pascal | Assigned To | => virgile |
2013-09-02 15:58 | svn | ||
2013-09-02 15:58 | svn | Status | assigned => resolved |
2013-09-02 15:58 | svn | Resolution | open => fixed |
2013-12-19 01:11 | Source_changeset_attached | => framac master 95cb344a | |
2014-02-12 16:53 | Source_changeset_attached | => framac stable/neon 95cb344a | |
2014-02-12 16:57 | Note Added: 0004561 | ||
2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
2014-03-13 15:57 | signoles | Status | resolved => closed |