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-09-01 13:38
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
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]
? file icon patch-downcast-rte [^] (2,233 bytes) 2017-09-01 13:33 [Show Content]

- Relationships

-  Notes
(0006457)
yakobowski (manager)
2017-09-01 13:21
edited on: 2017-09-01 13:38

The alarms for overflows are correct, because the computations occur on the int type. This is similar to

char a = ..., b = ...;
char c = a + b; // No overflow because the computation is char c = (char)((int)a+(int)b);

On the other hand, the assertions for downcasts are erroneous.

(0006458)
yakobowski (manager)
2017-09-01 13:33
edited on: 2017-09-01 13:37

The problem also occurs in conversion from floating-point values to integers.


- 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
2017-08-12 00:46 yakobowski Severity minor => major
2017-09-01 13:21 yakobowski Note Added: 0006457
2017-09-01 13:33 yakobowski Note Added: 0006458
2017-09-01 13:33 yakobowski File Added: patch-downcast-rte
2017-09-01 13:37 yakobowski Note Edited: 0006458 View Revisions
2017-09-01 13:38 yakobowski Note Edited: 0006457 View Revisions


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker