Frama-C Bug Tracking System - Frama-C
View Issue Details
0002152Frama-CKernelpublic2015-08-21 16:292015-08-21 16:29
pascal 
virgile 
normalminoralways
assignedopen 
 
 
0002152: With struct containing arrays, option -unspecified-access is too strict
The 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.
struct s { char t[3]; } s; int main() { s.t[2] = s.t[1] = 0; return 0; }
The 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.
No tags attached.
Issue History
2015-08-21 16:29pascalNew Issue
2015-08-21 16:29pascalStatusnew => assigned
2015-08-21 16:29pascalAssigned To => virgile

There are no notes attached to this issue.