File: main.c

package info (click to toggle)
cbmc 5.10-5
  • links: PTS
  • area: main
  • in suites: buster
  • size: 73,416 kB
  • sloc: cpp: 264,330; ansic: 38,268; java: 19,025; python: 4,539; yacc: 4,275; makefile: 2,547; lex: 2,394; sh: 932; perl: 525; xml: 289; pascal: 169
file content (74 lines) | stat: -rw-r--r-- 1,568 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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
#include <assert.h>

#ifdef __GNUC__
typedef int base_type;

typedef base_type v4si __attribute__((vector_size(16)));

typedef union
{
  v4si v;
  base_type members[4];
} vector_u;

int main()
{
  assert(sizeof(int)==4);
  assert(sizeof(v4si)==16);

  vector_u x, y, z;

  z.v=x.v+y.v;

  assert(z.members[0]==x.members[0]+y.members[0]);
  assert(z.members[1]==x.members[1]+y.members[1]);
  assert(z.members[2]==x.members[2]+y.members[2]);
  assert(z.members[3]==x.members[3]+y.members[3]);

  z.v=x.v-y.v;

  assert(z.members[0]==x.members[0]-y.members[0]);
  assert(z.members[1]==x.members[1]-y.members[1]);
  assert(z.members[2]==x.members[2]-y.members[2]);
  assert(z.members[3]==x.members[3]-y.members[3]);

  z.v=-x.v;

  assert(z.members[0]==-x.members[0]);
  assert(z.members[1]==-x.members[1]);
  assert(z.members[2]==-x.members[2]);
  assert(z.members[3]==-x.members[3]);

  z.v=~x.v;

  assert(z.members[0]==~x.members[0]);
  assert(z.members[1]==~x.members[1]);
  assert(z.members[2]==~x.members[2]);
  assert(z.members[3]==~x.members[3]);

  // build vector with typecast
  z.v=(v4si){ 0, 1, 2, 3 };
  assert(z.members[0]==0 && z.members[1]==1 && z.members[2]==2 && z.members[3]==3);

  // build vector with initializer
  v4si some_vector={ 10, 11, 12, 13 };
  z.v=some_vector;
  assert(z.members[0]==10 && z.members[1]==11 && z.members[2]==12 && z.members[3]==13);

  // same from one
  v4si other_vector={ 0 };
  z.v=other_vector;

  // an array of vectors
  v4si image[] = { other_vector };

  assert(z.members[1]==0);
}

#else

int main()
{
}

#endif