Fix double-locking in symbolic regression tests

sim642 · sim642 · commit c24821f83ada · 2024-12-10T16:03:10.000+02:00
diff --git a/tests/regression/06-symbeq/20-mult_accs_nr.c b/tests/regression/06-symbeq/20-mult_accs_nr.c
@@ -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;
 }
 
diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.c b/tests/regression/06-symbeq/21-mult_accs_rc.c
@@ -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;
 }
 
diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t
@@ -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)
@@ -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)

Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,7 @@ void t_fun(void arg) {`
`15`	`15`	`pthread_mutex_lock(&s->mutex);`
`16`	`16`	`s->data = 5; // NORACE`
`17`	`17`	`s->lore = 6; // NORACE`
`18`		`- pthread_mutex_lock(&s->mutex);`
	`18`	`+ pthread_mutex_unlock(&s->mutex);`
`19`	`19`	`return NULL;`
`20`	`20`	`}`
`21`	`21`
Original file line number	Diff line number	Diff line change
`@@ -14,7 +14,7 @@ void t_fun(void arg) {`
`14`	`14`	`pthread_mutex_lock(&s->mutex);`
`15`	`15`	`s = get_s();`
`16`	`16`	`s->data = 5; // RACE!`
`17`		`- pthread_mutex_lock(&s->mutex);`
	`17`	`+ pthread_mutex_unlock(&s->mutex);`
`18`	`18`	`return NULL;`
`19`	`19`	`}`
`20`	`20`