File: gcc_builtins.c

package info (click to toggle)
frama-c 20161101%2Bsilicon%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 42,324 kB
  • ctags: 35,695
  • sloc: ml: 200,142; ansic: 31,465; makefile: 2,334; sh: 1,643; lisp: 259; python: 85; asm: 26
file content (197 lines) | stat: -rw-r--r-- 4,577 bytes parent folder | download | duplicates (2)
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
/* run.config
   STDOPT: +"-machdep gcc_x86_32"
 */

#include "share/libc/stdint.h"

#define likely(x)  __builtin_expect((x),1)
#define unlikely(x)  __builtin_expect((x),0)

int16_t __sync_fetch_and_add_int16_t (int16_t *ptr, int16_t value,...)
{
  int16_t tmp = *ptr;
  *ptr += value;
  return tmp;
}
int16_t __sync_fetch_and_sub_int16_t (int16_t *ptr, int16_t value,...)
{
  int16_t tmp = *ptr;
  *ptr -= value;
  return tmp;
}

int32_t __sync_fetch_and_add_int32_t (int32_t *ptr, int32_t value,...)
{
  int32_t tmp = *ptr;
  *ptr += value;
  return tmp;
}

int32_t __sync_fetch_and_sub_int32_t (int32_t *ptr, int32_t value,...)
{
  int32_t tmp = *ptr;
  *ptr -= value;
  return tmp;
}

int64_t __sync_fetch_and_add_int64_t (int64_t *ptr, int64_t value,...)
{
  int64_t tmp = *ptr;
  *ptr += value;
  return tmp;
}

int64_t __sync_fetch_and_sub_int64_t (int64_t *ptr, int64_t value,...)
{
  int64_t tmp = *ptr;
  *ptr -= value;
  return tmp;
}

int16_t __sync_add_and_fetch_int16_t (int16_t *ptr, int16_t value,...)
{
  *ptr += value;
  return *ptr;
}

int16_t __sync_sub_and_fetch_int16_t (int16_t *ptr, int16_t value,...)
{
  *ptr -= value;
  return *ptr;
}

int32_t __sync_add_and_fetch_int32_t (int32_t *ptr, int32_t value,...)
{
  *ptr += value;
  return *ptr;
}

int32_t __sync_sub_and_fetch_int32_t (int32_t *ptr, int32_t value,...)
{
  *ptr -= value;
  return *ptr;
}

int64_t __sync_add_and_fetch_int64_t (int64_t *ptr, int64_t value,...)
{
  *ptr += value;
  return *ptr;
}

int64_t __sync_sub_and_fetch_int64_t (int64_t *ptr, int64_t value,...)
{
  *ptr -= value;
  return *ptr;
}

int __sync_bool_compare_and_swap_uint16_t (uint16_t *ptr, uint16_t oldval, uint16_t newval,...)
{
   if (*ptr == oldval) {
     *ptr = newval;
     return 1;
   } else {
     return 0;
   }
}

int __sync_bool_compare_and_swap_uint32_t (uint32_t *ptr, uint32_t oldval, uint32_t newval,...)
{
   if (*ptr == oldval) {
     *ptr = newval;
     return 1;
   } else {
     return 0;
   }
}

int __sync_bool_compare_and_swap_uint64_t (uint64_t *ptr, uint64_t oldval, uint64_t newval,...)
{
   if (*ptr == oldval) {
     *ptr = newval;
     return 1;
   } else {
     return 0;
   }
}

void main(void) {
  {
    int16_t content = 100;
    int16_t *ptr = &content;
    int16_t value = 33;
    int16_t result;
    result = __sync_fetch_and_add(ptr, value);
    /*@ assert result == 100 && content == 133; */
    result = __sync_fetch_and_add(ptr, -11);
    /*@ assert result == 133 && content == 122; */
    result = __sync_fetch_and_sub(ptr, value);
    /*@ assert result == 122 && content == 89; */
    result = __sync_fetch_and_sub(ptr, -11);
    /*@ assert result == 89 && content == 100; */
  }
  {
    int32_t content = 100;
    int32_t *ptr = &content;
    int32_t value = 33;
    int32_t result;
    result = __sync_fetch_and_add(ptr, value);
    /*@ assert result == 100 && content == 133; */
    result = __sync_fetch_and_add(ptr, -11);
    /*@ assert result == 133 && content == 122; */
    result = __sync_fetch_and_sub(ptr, value);
    /*@ assert result == 122 && content == 89; */
    result = __sync_fetch_and_sub(ptr, -11);
    /*@ assert result == 89 && content == 100; */
  }
  {
    int64_t content = 100;
    int64_t *ptr = &content;
    int64_t value = 33;
    int64_t result;
    result = __sync_fetch_and_add(ptr, value);
    /*@ assert result == 100 && content == 133; */
    result = __sync_fetch_and_add(ptr, -11);
    /*@ assert result == 133 && content == 122; */
    result = __sync_fetch_and_sub(ptr, value);
    /*@ assert result == 122 && content == 89; */
    result = __sync_fetch_and_sub(ptr, -11);
    /*@ assert result == 89 && content == 100; */
  }
  {
    uint16_t content = 100;
    uint16_t *ptr = &content;
    uint16_t oldval = 100;
    uint16_t newval = 133;
    int result;
    result = __sync_bool_compare_and_swap(ptr, oldval, newval);
    /*@ assert result == 1 && *ptr == newval; */
  }
  {
    uint32_t content = 100;
    uint32_t *ptr = &content;
    uint32_t oldval = 100;
    uint32_t newval = 133;
    int result;
    result = __sync_bool_compare_and_swap(ptr, oldval, newval);
    /*@ assert result == 1 && *ptr == newval; */
  }
  {
    uint64_t content = 100;
    uint64_t *ptr = &content;
    uint64_t oldval = 100;
    uint64_t newval = 133;
    int result;
    result = __sync_bool_compare_and_swap(ptr, oldval, newval);
    /*@ assert result == 1 && *ptr == newval; */
  }
  if (likely(4 == 4)) {
    int x = 1;
  }
  if (unlikely(3 == 4)) {
    int x = 0;
  }
  int x = 2;
  if (__builtin_expect(x++, x)) {
    int y = x;
  }
}