Fix incorrect unlock in witness/tm-inv-transfer tests

goblint · Oct 2, 2023 · 7857a68 · 7857a68
1 parent 15e6c3d
commit 7857a68
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 10 deletions.
diff --git a/tests/regression/56-witness/60-tm-inv-transfer-protection.c b/tests/regression/56-witness/60-tm-inv-transfer-protection.c
@@ -35,12 +35,12 @@ int main(void) {
   __goblint_check(g >= 40);
   __goblint_check(g <= 41); // UNKNOWN (lacks expressivity)
   pthread_mutex_unlock(&C);
-  pthread_mutex_unlock(&C);
-  
+  pthread_mutex_unlock(&B);
+
   pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
   __goblint_check(g <= 42); // UNKNOWN (widen)
   pthread_mutex_unlock(&C);
-  
+
   return 0;
 }
diff --git a/tests/regression/56-witness/61-tm-inv-transfer-mine.c b/tests/regression/56-witness/61-tm-inv-transfer-mine.c
@@ -35,12 +35,12 @@ int main(void) {
   __goblint_check(g >= 40);
   __goblint_check(g <= 41);
   pthread_mutex_unlock(&C);
-  pthread_mutex_unlock(&C);
-  
+  pthread_mutex_unlock(&B);
+
   pthread_mutex_lock(&C);
-  __goblint_check(g >= 40);
+  __goblint_check(g >= 40); // TODO why?
   __goblint_check(g <= 42);
   pthread_mutex_unlock(&C);
-  
+
   return 0;
 }
diff --git a/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c b/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c
@@ -35,12 +35,12 @@ int main(void) {
   __goblint_check(g >= 40);
   __goblint_check(g <= 41); // UNKNOWN (lacks expressivity)
   pthread_mutex_unlock(&C);
-  pthread_mutex_unlock(&C);
-  
+  pthread_mutex_unlock(&B);
+
   pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
   __goblint_check(g <= 42);
   pthread_mutex_unlock(&C);
-  
+
   return 0;
 }