Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000788Frama-CPlug-in > wppublic2011-04-12 08:592014-02-12 16:54
Reporterpatrick 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0001728)
patrick (developer)
2011-04-12 09:50
edited on: 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)
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.
(0001739)
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.

- 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 Checkin
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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker