Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002314Frama-CPlug-in > RTEpublic2017-06-26 10:282017-06-27 14:01
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002314: Incorrect overflow and cast assertions for bitfields
DescriptionThe following snippet:
struct STR { int num : 7; };

void foo(int a, long b) {
  struct STR s = { .num = 0 };
  s.num = b;
  s.num += a;
}

generates the following assertions
/*@ assert rte: signed_downcast: b ≤ 2147483647; */
/*@ assert rte: signed_downcast: -2147483648 ≤ b; */
s.num = (int)b;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
/*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
s.num = (int)((int)s.num + a);

The limits for s.num are incorrect, since s.num is a bitfield of 7 bits its limits should be [-64, 63]


Steps To Reproduceframa-c -machdep x86_64 file.c -rte -warn-signed-overflow -warn-signed-downcast -print
TagsNo tags attached.
Attached Filesc file icon b.c [^] (116 bytes) 2017-06-26 10:28 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-06-26 10:28 kvorobyov New Issue
2017-06-26 10:28 kvorobyov Status new => assigned
2017-06-26 10:28 kvorobyov Assigned To => signoles
2017-06-26 10:28 kvorobyov File Added: b.c


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker