Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit bf93949

Browse files
hernanponcedeleonhernanponcedeleon
committed
preprocessed files
1 parent df0d198 commit bf93949

File tree

8 files changed

+290
-148
lines changed

8 files changed

+290
-148
lines changed

‎c/ldv-races/race-2_5-container_of.i‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1690,12 +1690,12 @@ void *my_callback(void *arg) {
16901690
struct my_data *data;
16911691
data = ({ const typeof( ((struct my_data *)0)->dev ) *__mptr = (dev); (struct my_data *)( (char *)__mptr - ((unsigned long) &((struct my_data *)0)->dev) );});
16921692
pthread_mutex_lock (&data->lock);
1693-
__VERIFIER_atomic_begin();
1693+
__VERIFIER_atomic_begin();
16941694
data->shared.a = 1;
1695-
__VERIFIER_atomic_end();
1696-
__VERIFIER_atomic_begin();
1695+
__VERIFIER_atomic_end();
1696+
__VERIFIER_atomic_begin();
16971697
data->shared.b = data->shared.b + 1;
1698-
__VERIFIER_atomic_end();
1698+
__VERIFIER_atomic_end();
16991699
pthread_mutex_unlock (&data->lock);
17001700
return 0;
17011701
}

‎c/ldv-races/race-3_2-container_of-global.i‎

Lines changed: 65 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ typedef signed short int __int16_t;
88
typedef unsigned short int __uint16_t;
99
typedef signed int __int32_t;
1010
typedef unsigned int __uint32_t;
11-
typedef signed long int __int64_t;
12-
typedef unsigned long int __uint64_t;
11+
__extension__ typedef signed long long int __int64_t;
12+
__extension__ typedef unsigned long long int __uint64_t;
1313
typedef __int8_t __int_least8_t;
1414
typedef __uint8_t __uint_least8_t;
1515
typedef __int16_t __int_least16_t;
@@ -18,48 +18,49 @@ typedef __int32_t __int_least32_t;
1818
typedef __uint32_t __uint_least32_t;
1919
typedef __int64_t __int_least64_t;
2020
typedef __uint64_t __uint_least64_t;
21-
typedef long int __quad_t;
22-
typedef unsigned long int __u_quad_t;
23-
typedef long int __intmax_t;
24-
typedef unsigned long int __uintmax_t;
25-
typedef unsigned long int __dev_t;
26-
typedef unsigned int __uid_t;
27-
typedef unsigned int __gid_t;
28-
typedef unsigned long int __ino_t;
29-
typedef unsigned long int __ino64_t;
30-
typedef unsigned int __mode_t;
31-
typedef unsigned long int __nlink_t;
32-
typedef long int __off_t;
33-
typedef long int __off64_t;
34-
typedef int __pid_t;
35-
typedef struct { int __val[2]; } __fsid_t;
36-
typedef long int __clock_t;
37-
typedef unsigned long int __rlim_t;
38-
typedef unsigned long int __rlim64_t;
39-
typedef unsigned int __id_t;
40-
typedef long int __time_t;
41-
typedef unsigned int __useconds_t;
42-
typedef long int __suseconds_t;
43-
typedef int __daddr_t;
44-
typedef int __key_t;
45-
typedef int __clockid_t;
46-
typedef void * __timer_t;
47-
typedef long int __blksize_t;
48-
typedef long int __blkcnt_t;
49-
typedef long int __blkcnt64_t;
50-
typedef unsigned long int __fsblkcnt_t;
51-
typedef unsigned long int __fsblkcnt64_t;
52-
typedef unsigned long int __fsfilcnt_t;
53-
typedef unsigned long int __fsfilcnt64_t;
54-
typedef long int __fsword_t;
55-
typedef long int __ssize_t;
56-
typedef long int __syscall_slong_t;
57-
typedef unsigned long int __syscall_ulong_t;
21+
__extension__ typedef long long int __quad_t;
22+
__extension__ typedef unsigned long long int __u_quad_t;
23+
__extension__ typedef long long int __intmax_t;
24+
__extension__ typedef unsigned long long int __uintmax_t;
25+
__extension__ typedef __uint64_t __dev_t;
26+
__extension__ typedef unsigned int __uid_t;
27+
__extension__ typedef unsigned int __gid_t;
28+
__extension__ typedef unsigned long int __ino_t;
29+
__extension__ typedef __uint64_t __ino64_t;
30+
__extension__ typedef unsigned int __mode_t;
31+
__extension__ typedef unsigned int __nlink_t;
32+
__extension__ typedef long int __off_t;
33+
__extension__ typedef __int64_t __off64_t;
34+
__extension__ typedef int __pid_t;
35+
__extension__ typedef struct { int __val[2]; } __fsid_t;
36+
__extension__ typedef long int __clock_t;
37+
__extension__ typedef unsigned long int __rlim_t;
38+
__extension__ typedef __uint64_t __rlim64_t;
39+
__extension__ typedef unsigned int __id_t;
40+
__extension__ typedef long int __time_t;
41+
__extension__ typedef unsigned int __useconds_t;
42+
__extension__ typedef long int __suseconds_t;
43+
__extension__ typedef int __daddr_t;
44+
__extension__ typedef int __key_t;
45+
__extension__ typedef int __clockid_t;
46+
__extension__ typedef void * __timer_t;
47+
__extension__ typedef long int __blksize_t;
48+
__extension__ typedef long int __blkcnt_t;
49+
__extension__ typedef __int64_t __blkcnt64_t;
50+
__extension__ typedef unsigned long int __fsblkcnt_t;
51+
__extension__ typedef __uint64_t __fsblkcnt64_t;
52+
__extension__ typedef unsigned long int __fsfilcnt_t;
53+
__extension__ typedef __uint64_t __fsfilcnt64_t;
54+
__extension__ typedef int __fsword_t;
55+
__extension__ typedef int __ssize_t;
56+
__extension__ typedef long int __syscall_slong_t;
57+
__extension__ typedef unsigned long int __syscall_ulong_t;
5858
typedef __off64_t __loff_t;
5959
typedef char *__caddr_t;
60-
typedef long int __intptr_t;
61-
typedef unsigned int __socklen_t;
60+
__extension__ typedef int __intptr_t;
61+
__extension__ typedef unsigned int __socklen_t;
6262
typedef int __sig_atomic_t;
63+
__extension__ typedef __int64_t __time64_t;
6364
static __inline __uint16_t
6465
__bswap_16 (__uint16_t __bsx)
6566
{
@@ -90,7 +91,7 @@ __uint64_identity (__uint64_t __x)
9091
{
9192
return __x;
9293
}
93-
typedef long unsigned int size_t;
94+
typedef unsigned int size_t;
9495
typedef __time_t time_t;
9596
struct timespec
9697
{
@@ -227,28 +228,29 @@ struct __pthread_rwlock_arch_t
227228
unsigned int __writers_futex;
228229
unsigned int __pad3;
229230
unsigned int __pad4;
230-
int __cur_writer;
231-
int __shared;
231+
unsigned char __flags;
232+
unsigned char __shared;
232233
signed char __rwelision;
233-
unsigned char __pad1[7];
234-
unsigned long int __pad2;
235-
unsigned int __flags;
234+
unsigned char __pad2;
235+
int __cur_writer;
236236
};
237-
typedef struct __pthread_internal_list
237+
typedef struct __pthread_internal_slist
238238
{
239-
struct __pthread_internal_list *__prev;
240-
struct __pthread_internal_list *__next;
241-
} __pthread_list_t;
239+
struct __pthread_internal_slist *__next;
240+
} __pthread_slist_t;
242241
struct __pthread_mutex_s
243242
{
244243
int __lock ;
245244
unsigned int __count;
246245
int __owner;
247-
unsigned int __nusers;
248246
int __kind;
249247

250-
short __spins; short __elision;
251-
__pthread_list_t __list;
248+
unsigned int __nusers;
249+
__extension__ union
250+
{
251+
struct { short __espins; short __eelision; } __elision_data;
252+
__pthread_slist_t __list;
253+
};
252254

253255
};
254256
struct __pthread_cond_s
@@ -292,14 +294,14 @@ typedef unsigned int pthread_key_t;
292294
typedef int pthread_once_t;
293295
union pthread_attr_t
294296
{
295-
char __size[56];
297+
char __size[36];
296298
long int __align;
297299
};
298300
typedef union pthread_attr_t pthread_attr_t;
299301
typedef union
300302
{
301303
struct __pthread_mutex_s __data;
302-
char __size[40];
304+
char __size[24];
303305
long int __align;
304306
} pthread_mutex_t;
305307
typedef union
@@ -311,7 +313,7 @@ typedef union
311313
typedef union
312314
{
313315
struct __pthread_rwlock_arch_t __data;
314-
char __size[56];
316+
char __size[32];
315317
long int __align;
316318
} pthread_rwlock_t;
317319
typedef union
@@ -322,15 +324,15 @@ typedef union
322324
typedef volatile int pthread_spinlock_t;
323325
typedef union
324326
{
325-
char __size[32];
327+
char __size[20];
326328
long int __align;
327329
} pthread_barrier_t;
328330
typedef union
329331
{
330332
char __size[4];
331333
int __align;
332334
} pthread_barrierattr_t;
333-
typedef long int __jmp_buf[8];
335+
typedef int __jmp_buf[6];
334336
enum
335337
{
336338
PTHREAD_CREATE_JOINABLE,
@@ -498,11 +500,11 @@ struct __pthread_cleanup_frame
498500
int __cancel_type;
499501
};
500502
extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf)
501-
;
503+
__attribute__ ((__regparm__ (1)));
502504
extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf)
503-
;
505+
__attribute__ ((__regparm__ (1)));
504506
extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf)
505-
__attribute__ ((__noreturn__))
507+
__attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__))
506508
__attribute__ ((__weak__))
507509
;
508510
struct __jmp_buf_tag;
@@ -883,7 +885,7 @@ extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)
883885
extern int __uflow (FILE *);
884886
extern int __overflow (FILE *, int);
885887

886-
typedef int wchar_t;
888+
typedef long int wchar_t;
887889

888890
typedef enum
889891
{

‎c/pthread-atomic/dekker.i‎

Lines changed: 38 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -712,18 +712,37 @@ void *thr1(void *_) {
712712
int f2 = flag2;
713713
__VERIFIER_atomic_end();
714714
while (f2 >= 1) {
715+
__VERIFIER_atomic_begin();
715716
int t = turn;
717+
__VERIFIER_atomic_end();
716718
if (t != 0) {
719+
__VERIFIER_atomic_begin();
717720
flag1 = 0;
721+
__VERIFIER_atomic_end();
722+
__VERIFIER_atomic_begin();
718723
t = turn;
719-
while (t != 0) {};
724+
__VERIFIER_atomic_end();
725+
while (t != 0) {
726+
__VERIFIER_atomic_begin();
727+
t = turn;
728+
__VERIFIER_atomic_end();
729+
};
730+
__VERIFIER_atomic_begin();
720731
flag1 = 1;
732+
__VERIFIER_atomic_end();
721733
}
734+
__VERIFIER_atomic_begin();
735+
f2 = flag2;
736+
__VERIFIER_atomic_end();
722737
}
723738
x = 0;
724739
if (!(x<=0)) ERROR: reach_error();
740+
__VERIFIER_atomic_begin();
725741
turn = 1;
742+
__VERIFIER_atomic_end();
743+
__VERIFIER_atomic_begin();
726744
flag1 = 0;
745+
__VERIFIER_atomic_end();
727746
return 0;
728747
}
729748
void *thr2(void *_) {
@@ -734,17 +753,34 @@ void *thr2(void *_) {
734753
int f1 = flag1;
735754
__VERIFIER_atomic_end();
736755
while (f1 >= 1) {
756+
__VERIFIER_atomic_begin();
737757
int t = turn;
758+
__VERIFIER_atomic_end();
738759
if (t != 1) {
760+
__VERIFIER_atomic_begin();
739761
flag2 = 0;
762+
__VERIFIER_atomic_end();
763+
__VERIFIER_atomic_begin();
740764
t = turn;
741-
while (t != 1) {};
765+
__VERIFIER_atomic_end();
766+
while (t != 1) {
767+
__VERIFIER_atomic_begin();
768+
t = turn;
769+
__VERIFIER_atomic_end();
770+
};
771+
__VERIFIER_atomic_begin();
742772
flag2 = 1;
773+
__VERIFIER_atomic_end();
743774
}
775+
__VERIFIER_atomic_begin();
776+
f1 = flag1;
777+
__VERIFIER_atomic_end();
744778
}
745779
x = 1;
746780
if (!(x>=1)) ERROR: reach_error();
781+
__VERIFIER_atomic_begin();
747782
turn = 1;
783+
__VERIFIER_atomic_end();
748784
__VERIFIER_atomic_begin();
749785
flag2 = 0;
750786
__VERIFIER_atomic_end();

0 commit comments

Comments
 (0)