| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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. |
| Notes |
| Issue History |
|||
| 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 |
| Issue History |