File: main.c

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (59 lines) | stat: -rw-r--r-- 886 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
#include <assert.h>

typedef int INT;

typedef enum _INTEL_CACHE_TYPE {
    IntelCacheNull,
    IntelCacheTrace=10
} INTEL_CACHE_TYPE;

struct bft {
  unsigned int a:3;
  unsigned int b:1;
  signed int c:2;
  _Bool d:3;

  // an anonymous bitfield
  signed int :2;

  // with typedef
  INT x:1;

  // made of sizeof
  unsigned int abc: sizeof(int);

  // enums are integers!
  INTEL_CACHE_TYPE Type : 5;

  // and good as field sizes
  INTEL_CACHE_TYPE Field2 : IntelCacheTrace;
};

int main() {
  struct bft bf;

  assert(bf.a<=7);
  assert(bf.b<=1);
  assert(bf.c<=1);

  bf.a&=0;
  assert(bf.a==0);

  bf.a+=9;
  assert(bf.a==1);

  bf.a<<=1;
  assert(bf.a==2);

  bf.a>>=1;
  assert(bf.a==1);

  bf.d=2;
  assert(bf.d==1);

  // assignments have the underlying type
  assert(sizeof(bf.d=1)==sizeof(_Bool));
  assert(sizeof(bf.a+=1)==sizeof(unsigned));

  bf.Type=IntelCacheTrace;
}