minimise test

Author: polgreen

regression/goto-instrument/assembly_call_graph_test/main.c

@@ -1,37 +1,13 @@
-#ifdef SATABS
-#define assert(e) __CPROVER_assert(e,"error")
-#endif
-
-volatile int turn; // integer variable to hold the ID of the thread whose turn is it
-int x; // variable to test mutual exclusion
-volatile int flag1 = 0, flag2 = 0; // boolean flags
-
-void* thr1(void * arg) { // frontend produces 12 transitions from this thread. It would be better if it would produce only 8!
-  flag1 = 1;
-  turn = 1;
-  __asm__ __volatile__ ("mfence": : :"memory");
-  __CPROVER_assume(! (flag2==1 && turn==1) );
-  // begin: critical section
-  x = 0;
-  assert(x<=0);
-  // end: critical section
-  flag1 = 0;
+void* thr1(void * arg) {
+ __asm__ __volatile__ ("mfence": : :"memory");
 }
 
 void* thr2(void * arg) {
-  flag2 = 1;
-  turn = 0;
   __asm__ __volatile__ ("mfence": : :"memory");
-  __CPROVER_assume(! (flag1==1 && turn==0) );
-  // begin: critical section
-  x = 1;
-  assert (x>=1);
-  // end: critical section
-  flag2 = 0;
 }
 
 int main()
 {
-  __CPROVER_ASYNC_1: thr1(0);
+  thr1(0);
   thr2(0);
 }