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
Assigned Tovirgile 
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