Skip to content

Commit

Permalink
Add tests for library function races via NULL
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Sep 19, 2023
1 parent 4e83af9 commit c5136d1
Show file tree
Hide file tree
Showing 4 changed files with 219 additions and 0 deletions.
54 changes: 54 additions & 0 deletions tests/regression/05-lval_ls/20-race-null-void.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
#include <pthread.h>
#include <stdio.h>

void *t_fun(void *arg) {
void **top;
free(top); // RACE
return NULL;
}

int main(void) {
pthread_t id;
pthread_create(&id, NULL, t_fun, NULL);

int r; // rand
int zero = 0; // IntDomain zero
void *null;
__goblint_assume(null == NULL); // AddressDomain NULL
int one = 1; // IntDomain one
void *unknown;
__goblint_assume(unknown != NULL); // AddressDomain unknown
void *top;
switch (r) {
case 0:
pthread_join(id, NULL); // NORACE
break;
case 1:
pthread_join(id, 0); // NORACE
break;
case 2:
pthread_join(id, zero); // NORACE
break;
case 3:
pthread_join(id, 1); // RACE
break;
case 4:
pthread_join(id, one); // RACE
break;
case 5:
pthread_join(id, r); // RACE
break;
case 6:
pthread_join(id, null); // NORACE
break;
case 7:
pthread_join(id, unknown); // RACE
break;
case 8:
pthread_join(id, top); // RACE
break;
default:
break;
}
return 0;
}
55 changes: 55 additions & 0 deletions tests/regression/05-lval_ls/21-race-null-type.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
// PARAM: --enable ana.race.direct-arithmetic
#include <pthread.h>
#include <stdio.h>

void *t_fun(void *arg) {
void *top;
time(top); // RACE
return NULL;
}

int main(void) {
pthread_t id;
pthread_create(&id, NULL, t_fun, NULL);

int r; // rand
int zero = 0; // IntDomain zero
void *null;
__goblint_assume(null == NULL); // AddressDomain NULL
int one = 1; // IntDomain one
void *unknown;
__goblint_assume(unknown != NULL); // AddressDomain unknown
void *top;
switch (r) {
case 0:
time(NULL); // NORACE
break;
case 1:
time(0); // NORACE
break;
case 2:
time(zero); // NORACE
break;
case 3:
time(1); // RACE
break;
case 4:
time(one); // RACE
break;
case 5:
time(r); // RACE
break;
case 6:
time(null); // NORACE
break;
case 7:
time(unknown); // RACE
break;
case 8:
time(top); // RACE
break;
default:
break;
}
return 0;
}
56 changes: 56 additions & 0 deletions tests/regression/05-lval_ls/22-race-null-void-deep.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
#include <pthread.h>
#include <stdio.h>

pthread_key_t key;

void *t_fun(void *arg) {
void *top;
pthread_setspecific(key, top); // RACE
return NULL;
}

int main(void) {
pthread_t id;
pthread_create(&id, NULL, t_fun, NULL);

int r; // rand
int zero = 0; // IntDomain zero
void *null;
__goblint_assume(null == NULL); // AddressDomain NULL
int one = 1; // IntDomain one
void *unknown;
__goblint_assume(unknown != NULL); // AddressDomain unknown
void *top;
switch (r) {
case 0:
pthread_setspecific(key, NULL); // NORACE
break;
case 1:
pthread_setspecific(key, 0); // NORACE
break;
case 2:
pthread_setspecific(key, zero); // NORACE
break;
case 3:
pthread_setspecific(key, 1); // RACE
break;
case 4:
pthread_setspecific(key, one); // RACE
break;
case 5:
pthread_setspecific(key, r); // RACE
break;
case 6:
pthread_setspecific(key, null); // NORACE
break;
case 7:
pthread_setspecific(key, unknown); // RACE
break;
case 8:
pthread_setspecific(key, top); // RACE
break;
default:
break;
}
return 0;
}
54 changes: 54 additions & 0 deletions tests/regression/05-lval_ls/23-race-null-type-deep.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
#include <pthread.h>
#include <stdio.h>

void *t_fun(void *arg) {
void *top;
fclose(top); // RACE
return NULL;
}

int main(void) {
pthread_t id;
pthread_create(&id, NULL, t_fun, NULL);

int r; // rand
int zero = 0; // IntDomain zero
void *null;
__goblint_assume(null == NULL); // AddressDomain NULL
int one = 1; // IntDomain one
void *unknown;
__goblint_assume(unknown != NULL); // AddressDomain unknown
void *top;
switch (r) {
case 0:
feof(NULL); // NORACE
break;
case 1:
feof(0); // NORACE
break;
case 2:
feof(zero); // NORACE
break;
case 3:
feof(1); // RACE
break;
case 4:
feof(one); // RACE
break;
case 5:
feof(r); // RACE
break;
case 6:
feof(null); // NORACE
break;
case 7:
feof(unknown); // RACE
break;
case 8:
feof(top); // RACE
break;
default:
break;
}
return 0;
}

0 comments on commit c5136d1

Please sign in to comment.