Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002152Frama-CKernelpublic2015-08-21 16:292015-08-21 16:29
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002152: With struct containing arrays, option -unspecified-access is too strict
DescriptionThe program given below is correct, but: $ frama-c -val t.c -unspecified-access ... t.c:4:[kernel] warning: Unspecified sequence with side effect: /* s.t[1] <- s.t */ s.t[1] = (char)0; /* s.t[2] <- s.t */ s.t[2] = s.t[1]; [value] Analyzing a complete application starting at main ... t.c:4:[kernel] warning: undefined multiple accesses in expression. assert \separated(&s.t[1], &s.t); [value] Recording results for main [value] done for function main t.c:4:[value] Assertion 'Value,separation' got final status invalid. ... I expected this program would be accepted without a warning about multiple accesses in expressions.
Steps To Reproducestruct s { char t[3]; } s; int main() { s.t[2] = s.t[1] = 0; return 0; }
Additional InformationThe struct is necessary for the bug to appear. With a toplevel array t, the assignment t[2] = t[1] = 0; does not cause a warning.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-08-21 16:29 pascal New Issue
2015-08-21 16:29 pascal Status new => assigned
2015-08-21 16:29 pascal Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker