expsplit-test

Author: Simon Tietz

tests/practical/expsplit.c renamed to tests/regression/07-asm-exp-split.c

@@ -1,3 +1,4 @@
+// PARAM: --set ana.activated[+] expsplit --disable asm_is_nop
 #include <goblint.h>
 
 int main(void) {
@@ -7,5 +8,5 @@ int main(void) {
   asm("nop" : "=x" (x), "=x" (r));
   __goblint_check(x == 0 || x == 1);
   __goblint_split_end(x);
-  __goblint_check(x == 0 || x == 1);
+  __goblint_check(x == 0 || x == 1); // UNKNOWN (intentionally)
 }

tests/regression/79-assembly/28-asm_deadlock.c

@@ -2,17 +2,13 @@
 #include <unistd.h>
 #include <pthread.h>
 #include <stdio.h>
-#include <goblint.h>
 
 pthread_mutex_t lock_a;
 pthread_mutex_t lock_b;
 
-extern __goblint_unknown(void*);
-
 void *proc_a(void *arg) {
-    asm ("nop" : "=g" (lock_a));
-    __goblint_unknown(&lock_a);
     pthread_mutex_lock(&lock_a);
+    asm ("nop" : "=g" (lock_a));
     sleep(1);
     pthread_mutex_lock(&lock_b);
     pthread_exit(NULL);