2021-03-01 04:16 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000823Frama-CKernelpublic2011-05-12 14:292014-02-12 16:59
Reporterpascal 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000823: r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (csmith)
Description#include <stdio.h>

struct S { unsigned f:32; } x = { 28349};

unsigned short us = 0xDC23L;

main(){
  int r = (x.f ^ ((short)-87)) >= us;
  printf("%d\n", r);
  return r;
}

gcc w.c && ./a.out
1

But:

~/ppc/bin/toplevel.opt -print w.c | grep -v preprocessing > w2.c && gcc w2.c && ./a.out
0

The front-end is correct in typing unsigned bit-fields as int most of the time, but there should be an exception for unsigned bit-fields of size 32. See http://stackoverflow.com/q/5977456/139746
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0001877

pascal (reporter)

2011-05-12 18:56

Last edited: 2011-05-12 18:56

 You have forgotten "unsigned" before "bitfields which have a size equal to the size of int" in your commit message.

Unfortunately, you have also forgotten to handle signed 32-bit bitfields in your patch.

Try the following :

Manzana:~ pascal$ ~/ppc/bin/toplevel.byte -val t.c
...
[value] Values for function main:
          r ? {1}
Manzana:~ pascal$ gcc t.c
Manzana:~ pascal$ ./a.out
0
Manzana:~ pascal$ clang t.c
t.c:7:1: warning: type specifier missing, defaults to 'int' [-Wimplicit-int]
main(){
^
1 warning generated.
Manzana:~ pascal$ ./a.out
0
Manzana:~ pascal$ cat t.c
#include <stdio.h>

struct S { signed f:32; } x = { 28349};

unsigned short us = 0xDC23L;

main(){
  int r = (x.f ^ ((short)-87)) >= us;
  printf("%d\n", r);
  return r;
}

~0004791

monate (reporter)

2014-02-12 16:59

 Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-05-12 14:29 pascal New Issue
2011-05-12 14:30 pascal Status new => assigned
2011-05-12 14:30 pascal Assigned To => monate
2011-05-12 15:31 svn
2011-05-12 15:31 svn Status assigned => resolved
2011-05-12 15:31 svn Resolution open => fixed
2011-05-12 18:56 pascal Note Added: 0001877
2011-05-12 18:56 pascal Status resolved => feedback
2011-05-12 18:56 pascal Resolution fixed => reopened
2011-05-12 18:56 pascal Note Edited: 0001877
2011-05-12 18:57 pascal Status feedback => confirmed
2011-05-13 15:23 svn
2011-05-13 16:14 monate Status confirmed => resolved
2011-05-13 16:14 monate Resolution reopened => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 svn Source_changeset_attached => framac master 5ac9203a
2013-12-19 01:12 svn Source_changeset_attached => framac master 8b0d56b2
2014-02-12 16:54 monate Source_changeset_attached => framac stable/neon 5ac9203a
2014-02-12 16:54 monate Source_changeset_attached => framac stable/neon 8b0d56b2
2014-02-12 16:59 monate Note Added: 0004791
2014-02-12 16:59 monate Status closed => resolved
+Issue History