View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000788 | Frama-C | Plug-in > wp | public | 2011-04-12 08:59 | 2014-02-12 16:54 | ||||
Reporter | patrick | ||||||||
Assigned To | dargaye | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Carbon-20110201 | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000788: initializer completion | ||||||||
Description | C initialization of globals should be completed by 0. This is partially done by CIL, since int t15[15] = {3} ; int t20[20] = {3} ; is translated into int t15[15] = {3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; int t20[20] = {3}; So, it can (maybe not for big arrays) be a bug of CIL. Otherwise, wp should virtually perform this completion. This is not done by wp 0.3 plug-in | ||||||||
Additional Information | This ensures clause should be provable. int t15[15] = {3} ; int t20[20] = {3} ; //@ ensures t20[3]==0; int main (void) { } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
patrick (developer) 2011-04-12 09:50 Last edited: 2011-04-12 13:33 |
Notice the value analysis is able to prove that property. [Value] should perform this kind of completion, not always done by [CIL]. [WP] should do the same kind of completion in the generated POs. |
pascal (reporter) 2011-04-12 12:42 |
There is a good reason for not generating the final zeroes automatically: it takes the programmer a short time to write int t[100000] = { 1 }; , so he expects the analyzer to be as fast on this program. Each plug-in that needs to give a meaning to global definitions should have its own routine to create zeroed areas, as efficient as possible. |
patrick (developer) 2011-04-12 15:33 |
As suggested by Pascal, the completion do not require any expansion. WP can consider that the C initializer as functional update of the specified elements upon an initial value filled with zeros. These initial zero values can be defined implicitly through axioms. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-04-12 08:59 | patrick | New Issue | |
2011-04-12 08:59 | patrick | Status | new => assigned |
2011-04-12 08:59 | patrick | Assigned To | => dargaye |
2011-04-12 09:50 | patrick | Note Added: 0001728 | |
2011-04-12 12:42 | pascal | Note Added: 0001737 | |
2011-04-12 13:31 | patrick | Description Updated | |
2011-04-12 13:33 | patrick | Note Edited: 0001728 | |
2011-04-12 15:33 | patrick | Note Added: 0001739 | |
2011-04-13 11:23 | svn | ||
2011-05-27 14:16 | dargaye | Status | assigned => resolved |
2011-05-27 14:16 | dargaye | Resolution | open => fixed |
2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
2011-10-10 14:14 | signoles | Status | resolved => closed |
2013-12-19 01:12 | correnson | Source_changeset_attached | => framac master 8dc2d45f |
2014-02-12 16:54 | correnson | Source_changeset_attached | => framac stable/neon 8dc2d45f |