Skip to content

Commit 626ec9f

Browse files
author
Peter Schrammel
committed
more line terminators
1 parent 881c3f2 commit 626ec9f

File tree

15 files changed

+603
-603
lines changed

15 files changed

+603
-603
lines changed

‎regression/cbmc-concurrency/deadlock1/main.c

+22-22
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,22 @@
1-
#include <pthread.h>
2-
#include <stdlib.h>
3-
#include <assert.h>
4-
5-
pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
6-
7-
void* lock_never_unlock_002_tsk_001(void* pram) {
8-
pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);
9-
return NULL;
10-
}
11-
12-
void main() {
13-
pthread_t tid1;
14-
pthread_t tid2;
15-
pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL);
16-
pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL);
17-
pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL);
18-
pthread_join(tid1, NULL);
19-
pthread_join(tid2, NULL);
20-
// deadlock in the threads; assertion should not be reachable
21-
assert(0);
22-
}
1+
#include <pthread.h>
2+
#include <stdlib.h>
3+
#include <assert.h>
4+
5+
pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
6+
7+
void* lock_never_unlock_002_tsk_001(void* pram) {
8+
pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);
9+
return NULL;
10+
}
11+
12+
void main() {
13+
pthread_t tid1;
14+
pthread_t tid2;
15+
pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL);
16+
pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL);
17+
pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL);
18+
pthread_join(tid1, NULL);
19+
pthread_join(tid2, NULL);
20+
// deadlock in the threads; assertion should not be reachable
21+
assert(0);
22+
}

‎regression/cbmc-concurrency/deadlock2/main.c

+23-23
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
1-
#include <pthread.h>
2-
#include <stdlib.h>
3-
#include <assert.h>
4-
5-
pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
6-
7-
void* lock_never_unlock_002_tsk_001(void* pram) {
8-
pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);
9-
pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);
10-
return NULL;
11-
}
12-
13-
void main() {
14-
pthread_t tid1;
15-
pthread_t tid2;
16-
pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL);
17-
pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL);
18-
pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL);
19-
pthread_join(tid1, NULL);
20-
pthread_join(tid2, NULL);
21-
// no deadlock in the threads; assertion should be reached
22-
assert(0);
23-
}
1+
#include <pthread.h>
2+
#include <stdlib.h>
3+
#include <assert.h>
4+
5+
pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
6+
7+
void* lock_never_unlock_002_tsk_001(void* pram) {
8+
pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);
9+
pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);
10+
return NULL;
11+
}
12+
13+
void main() {
14+
pthread_t tid1;
15+
pthread_t tid2;
16+
pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL);
17+
pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL);
18+
pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL);
19+
pthread_join(tid1, NULL);
20+
pthread_join(tid2, NULL);
21+
// no deadlock in the threads; assertion should be reached
22+
assert(0);
23+
}

‎regression/cbmc-concurrency/norace_array1/main.c

+26-26
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,26 @@
1-
#include <pthread.h>
2-
#include <assert.h>
3-
4-
int s[2];
5-
6-
void* thread_0(void* arg)
7-
{
8-
s[0] = 2;
9-
assert(s[0] == 2);
10-
return NULL;
11-
}
12-
13-
void* thread_1(void* arg)
14-
{
15-
s[1] = 1;
16-
assert(s[1] == 1);
17-
return NULL;
18-
}
19-
20-
int main(void)
21-
{
22-
pthread_t thread0, thread1;
23-
pthread_create(&thread0, NULL, thread_0, 0);
24-
pthread_create(&thread1, NULL, thread_1, 0);
25-
return 0;
26-
}
1+
#include <pthread.h>
2+
#include <assert.h>
3+
4+
int s[2];
5+
6+
void* thread_0(void* arg)
7+
{
8+
s[0] = 2;
9+
assert(s[0] == 2);
10+
return NULL;
11+
}
12+
13+
void* thread_1(void* arg)
14+
{
15+
s[1] = 1;
16+
assert(s[1] == 1);
17+
return NULL;
18+
}
19+
20+
int main(void)
21+
{
22+
pthread_t thread0, thread1;
23+
pthread_create(&thread0, NULL, thread_0, 0);
24+
pthread_create(&thread1, NULL, thread_1, 0);
25+
return 0;
26+
}

‎regression/cbmc-concurrency/norace_scalar1/main.c

+26-26
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,26 @@
1-
#include <pthread.h>
2-
#include <assert.h>
3-
4-
int f0, f1;
5-
6-
void* thread_0(void* arg)
7-
{
8-
f0 = 2;
9-
assert(f0 == 2);
10-
return NULL;
11-
}
12-
13-
void* thread_1(void* arg)
14-
{
15-
f1 = 1;
16-
assert(f1 == 1);
17-
return NULL;
18-
}
19-
20-
int main(void)
21-
{
22-
pthread_t thread0, thread1;
23-
pthread_create(&thread0, NULL, thread_0, 0);
24-
pthread_create(&thread1, NULL, thread_1, 0);
25-
return 0;
26-
}
1+
#include <pthread.h>
2+
#include <assert.h>
3+
4+
int f0, f1;
5+
6+
void* thread_0(void* arg)
7+
{
8+
f0 = 2;
9+
assert(f0 == 2);
10+
return NULL;
11+
}
12+
13+
void* thread_1(void* arg)
14+
{
15+
f1 = 1;
16+
assert(f1 == 1);
17+
return NULL;
18+
}
19+
20+
int main(void)
21+
{
22+
pthread_t thread0, thread1;
23+
pthread_create(&thread0, NULL, thread_0, 0);
24+
pthread_create(&thread1, NULL, thread_1, 0);
25+
return 0;
26+
}

‎regression/cbmc-concurrency/norace_struct1/main.c

+26-26
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,26 @@
1-
#include <pthread.h>
2-
#include <assert.h>
3-
4-
struct { int f0; int f1; } s;
5-
6-
void* thread_0(void* arg)
7-
{
8-
s.f0 = 2;
9-
assert(s.f0 == 2);
10-
return NULL;
11-
}
12-
13-
void* thread_1(void* arg)
14-
{
15-
s.f1 = 1;
16-
assert(s.f1 == 1);
17-
return NULL;
18-
}
19-
20-
int main(void)
21-
{
22-
pthread_t thread0, thread1;
23-
pthread_create(&thread0, NULL, thread_0, 0);
24-
pthread_create(&thread1, NULL, thread_1, 0);
25-
return 0;
26-
}
1+
#include <pthread.h>
2+
#include <assert.h>
3+
4+
struct { int f0; int f1; } s;
5+
6+
void* thread_0(void* arg)
7+
{
8+
s.f0 = 2;
9+
assert(s.f0 == 2);
10+
return NULL;
11+
}
12+
13+
void* thread_1(void* arg)
14+
{
15+
s.f1 = 1;
16+
assert(s.f1 == 1);
17+
return NULL;
18+
}
19+
20+
int main(void)
21+
{
22+
pthread_t thread0, thread1;
23+
pthread_create(&thread0, NULL, thread_0, 0);
24+
pthread_create(&thread1, NULL, thread_1, 0);
25+
return 0;
26+
}

‎regression/cbmc-concurrency/struct_and_array1/main.c

+40-40
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,40 @@
1-
#include <pthread.h>
2-
3-
typedef struct st_t
4-
{
5-
unsigned char x;
6-
unsigned char y;
7-
} ST;
8-
9-
ST st;
10-
11-
char my_array[10];
12-
13-
_Bool done1, done2;
14-
15-
void *foo1(void *arg1)
16-
{
17-
st.x = 1;
18-
my_array[1]=1;
19-
done1 = 1;
20-
}
21-
22-
void *foo2(void *arg2)
23-
{
24-
st.y = 1;
25-
my_array[2]=2;
26-
done2 = 1;
27-
}
28-
29-
int main()
30-
{
31-
pthread_t t;
32-
pthread_create(&t,NULL,foo1,NULL);
33-
pthread_create(&t,NULL,foo2,NULL);
34-
35-
if(done1 && done2)
36-
{
37-
assert(st.x==st.y);
38-
assert(my_array[1]==my_array[2]);
39-
}
40-
}
1+
#include <pthread.h>
2+
3+
typedef struct st_t
4+
{
5+
unsigned char x;
6+
unsigned char y;
7+
} ST;
8+
9+
ST st;
10+
11+
char my_array[10];
12+
13+
_Bool done1, done2;
14+
15+
void *foo1(void *arg1)
16+
{
17+
st.x = 1;
18+
my_array[1]=1;
19+
done1 = 1;
20+
}
21+
22+
void *foo2(void *arg2)
23+
{
24+
st.y = 1;
25+
my_array[2]=2;
26+
done2 = 1;
27+
}
28+
29+
int main()
30+
{
31+
pthread_t t;
32+
pthread_create(&t,NULL,foo1,NULL);
33+
pthread_create(&t,NULL,foo2,NULL);
34+
35+
if(done1 && done2)
36+
{
37+
assert(st.x==st.y);
38+
assert(my_array[1]==my_array[2]);
39+
}
40+
}

‎regression/cbmc-from-CVS/Struct_Pointer2/main.c

+27-27
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,27 @@
1-
#include <stdlib.h>
2-
#include <assert.h>
3-
4-
struct mylist
5-
{
6-
int data;
7-
struct mylist *next;
8-
};
9-
10-
int main()
11-
{
12-
struct mylist *p;
13-
14-
// Allocations:
15-
p=malloc( sizeof(struct mylist ) );
16-
p->data=1;
17-
p->next=malloc( sizeof(struct mylist ) );
18-
p->next->data=2;
19-
p->next->next=malloc( sizeof(struct mylist ) );
20-
p->next->next->data=3;
21-
p->next->next->next=malloc( sizeof(struct mylist ) );
22-
p->next->next->next->data=4;
23-
24-
assert(p->next->next->data==3);
25-
26-
return 0;
27-
}
1+
#include <stdlib.h>
2+
#include <assert.h>
3+
4+
struct mylist
5+
{
6+
int data;
7+
struct mylist *next;
8+
};
9+
10+
int main()
11+
{
12+
struct mylist *p;
13+
14+
// Allocations:
15+
p=malloc( sizeof(struct mylist ) );
16+
p->data=1;
17+
p->next=malloc( sizeof(struct mylist ) );
18+
p->next->data=2;
19+
p->next->next=malloc( sizeof(struct mylist ) );
20+
p->next->next->data=3;
21+
p->next->next->next=malloc( sizeof(struct mylist ) );
22+
p->next->next->next->data=4;
23+
24+
assert(p->next->next->data==3);
25+
26+
return 0;
27+
}

0 commit comments

Comments
 (0)