2021-03-02 02:08 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000788Frama-CPlug-in > wppublic2014-02-12 16:54
Reporterpatrick 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000788: initializer completion
DescriptionC 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 InformationThis ensures clause should be provable.
int t15[15] = {3} ;
int t20[20] = {3} ;
//@ ensures t20[3]==0;
int main (void) { }
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0001728

patrick (developer)

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.

~0001737

pascal (reporter)

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.

~0001739

patrick (developer)

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