Skip to content

Commit

Permalink
Fix double-locking in symbolic regression tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Dec 10, 2024
1 parent 55e4973 commit c24821f
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 6 deletions.
2 changes: 1 addition & 1 deletion tests/regression/06-symbeq/20-mult_accs_nr.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ void *t_fun(void *arg) {
pthread_mutex_lock(&s->mutex);
s->data = 5; // NORACE
s->lore = 6; // NORACE
pthread_mutex_lock(&s->mutex);
pthread_mutex_unlock(&s->mutex);
return NULL;
}

Expand Down
2 changes: 1 addition & 1 deletion tests/regression/06-symbeq/21-mult_accs_rc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ void *t_fun(void *arg) {
pthread_mutex_lock(&s->mutex);
s = get_s();
s->data = 5; // RACE!
pthread_mutex_lock(&s->mutex);
pthread_mutex_unlock(&s->mutex);
return NULL;
}

Expand Down
10 changes: 6 additions & 4 deletions tests/regression/06-symbeq/21-mult_accs_rc.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,16 @@ Disable info messages because race summary contains (safe) memory location count
$ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 21-mult_accs_rc.c 2>&1 | tee default-output-1.txt
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:14:3-14:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:16:3-16:14)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:17:3-17:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:17:3-17:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:28:3-28:16)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9)
[Warning][Race] Memory location (struct s).data (race with conf. 100):
write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
[Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32)
[Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:17:3-17:32)
[Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:17:3-17:34)
[Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:17:3-17:34)
[Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:33:3-33:24)
[Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:35:3-35:26)
[Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26)
Expand All @@ -23,14 +24,15 @@ Disable info messages because race summary contains (safe) memory location count
$ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 21-mult_accs_rc.c 2>&1 | tee default-output-2.txt
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:14:3-14:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:16:3-16:14)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:17:3-17:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:17:3-17:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:28:3-28:16)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9)
[Success][Race] Memory location (struct s).data (safe):
write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
[Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32)
[Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:17:3-17:32)
[Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:17:3-17:34)
[Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:17:3-17:34)
[Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:33:3-33:24)
[Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:35:3-35:26)
[Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26)
Expand Down

0 comments on commit c24821f

Please sign in to comment.