Updated: systemc. 08 -> 09.

UnitTestBot · Apr 22, 2024 · f996c31 · f996c31
1 parent bb2533a
commit f996c31
Showing 1 changed file with 135 additions and 10 deletions.
diff --git a/systemc/token_ring.09.cil-2.c b/systemc/token_ring.09.cil-2.c
@@ -43,6 +43,7 @@ int t5_pc  =    0;
 int t6_pc  =    0;
 int t7_pc  =    0;
 int t8_pc  =    0;
+int t9_pc  =    0;
 int m_st  ;
 int t1_st  ;
 int t2_st  ;
@@ -52,6 +53,7 @@ int t5_st  ;
 int t6_st  ;
 int t7_st  ;
 int t8_st  ;
+int t9_st  ;
 int m_i  ;
 int t1_i  ;
 int t2_i  ;
@@ -61,6 +63,7 @@ int t5_i  ;
 int t6_i  ;
 int t7_i  ;
 int t8_i  ;
+int t9_i  ;
 int M_E  =    2;
 int T1_E  =    2;
 int T2_E  =    2;
@@ -70,6 +73,7 @@ int T5_E  =    2;
 int T6_E  =    2;
 int T7_E  =    2;
 int T8_E  =    2;
+int T9_E  =    2;
 int E_M  =    2;
 int E_1  =    2;
 int E_2  =    2;
@@ -79,6 +83,7 @@ int E_5  =    2;
 int E_6  =    2;
 int E_7  =    2;
 int E_8  =    2;
+int E_9  =    2;
 int is_master_triggered(void) ;
 int is_transmit1_triggered(void) ;
 int is_transmit2_triggered(void) ;
@@ -88,6 +93,7 @@ int is_transmit5_triggered(void) ;
 int is_transmit6_triggered(void) ;
 int is_transmit7_triggered(void) ;
 int is_transmit8_triggered(void) ;
+int is_transmit9_triggered(void) ;
 void immediate_notify(void) ;
 int token  ;
 int __VERIFIER_nondet_int()  ;
@@ -121,7 +127,7 @@ void master(void)
 
     goto return_label;
     M_WAIT: ;
-    if (token != local + 8) {
+    if (token != local + 9) {
       {
       error();
       }
@@ -424,12 +430,48 @@ void transmit8(void)
     T8_WAIT: 
     {
     token += 1;
+    E_9 = 1;
+    immediate_notify();
+    E_9 = 2;
+    }
+  }
+  while_8_break: /* CIL Label */ ;
+  }
+
+  return_label: /* CIL Label */ 
+  return;
+}
+}
+void transmit9(void) 
+{ 
+
+  {
+  if (t9_pc == 0) {
+    goto T9_ENTRY;
+  } else {
+    if (t9_pc == 1) {
+      goto T9_WAIT;
+    } else {
+
+    }
+  }
+  T9_ENTRY: ;
+  {
+  while (1) {
+    while_9_continue: /* CIL Label */ ;
+    t9_pc = 1;
+    t9_st = 2;
+
+    goto return_label;
+    T9_WAIT: 
+    {
+    token += 1;
     E_M = 1;
     immediate_notify();
     E_M = 2;
     }
   }
-  while_8_break: /* CIL Label */ ;
+  while_9_break: /* CIL Label */ ;
   }
 
   return_label: /* CIL Label */ 
@@ -607,6 +649,25 @@ int is_transmit8_triggered(void)
   return (__retres1);
 }
 }
+int is_transmit9_triggered(void) 
+{ int __retres1 ;
+
+  {
+  if (t9_pc == 1) {
+    if (E_9 == 1) {
+      __retres1 = 1;
+      goto return_label;
+    } else {
+
+    }
+  } else {
+
+  }
+  __retres1 = 0;
+  return_label: /* CIL Label */ 
+  return (__retres1);
+}
+}
 void update_channels(void) 
 { 
 
@@ -664,6 +725,11 @@ void init_threads(void)
   } else {
     t8_st = 2;
   }
+  if (t9_i == 1) {
+    t9_st = 0;
+  } else {
+    t9_st = 2;
+  }
 
   return;
 }
@@ -708,7 +774,12 @@ int exists_runnable_thread(void)
                     __retres1 = 1;
                     goto return_label;
                   } else {
+                    if (t9_st == 0) {
+                      __retres1 = 1;
+                      goto return_label;
+                    } else {
 
+                    }
                   }
                 }
               }
@@ -730,14 +801,14 @@ void eval(void)
   {
   {
   while (1) {
-    while_9_continue: /* CIL Label */ ;
+    while_10_continue: /* CIL Label */ ;
     {
     tmp = exists_runnable_thread();
     }
     if (tmp) {
 
     } else {
-      goto while_9_break;
+      goto while_10_break;
     }
     if (m_st == 0) {
       int tmp_ndt_1;
@@ -768,7 +839,7 @@ void eval(void)
 
     }
     if (t2_st == 0) {
-      int tmp_ndt_3;
+        int tmp_ndt_3;
       tmp_ndt_3 = __VERIFIER_nondet_int();
       if (tmp_ndt_3) {
         {
@@ -864,9 +935,23 @@ void eval(void)
       }
     } else {
 
+    }
+    if (t9_st == 0) {
+      int tmp_ndt_10;
+      tmp_ndt_10 = __VERIFIER_nondet_int();
+      if (tmp_ndt_10) {
+        {
+        t9_st = 1;
+        transmit9();
+        }
+      } else {
+
+      }
+    } else {
+
     }
   }
-  while_9_break: /* CIL Label */ ;
+  while_10_break: /* CIL Label */ ;
   }
 
   return;
@@ -920,6 +1005,11 @@ void fire_delta_events(void)
     T8_E = 1;
   } else {
 
+  }
+  if (T9_E == 0) {
+    T9_E = 1;
+  } else {
+
   }
   if (E_M == 0) {
     E_M = 1;
@@ -965,6 +1055,11 @@ void fire_delta_events(void)
     E_8 = 1;
   } else {
 
+  }
+  if (E_9 == 0) {
+    E_9 = 1;
+  } else {
+
   }
 
   return;
@@ -1018,6 +1113,11 @@ void reset_delta_events(void)
     T8_E = 2;
   } else {
 
+  }
+  if (T9_E == 1) {
+    T9_E = 2;
+  } else {
+
   }
   if (E_M == 1) {
     E_M = 2;
@@ -1063,6 +1163,11 @@ void reset_delta_events(void)
     E_8 = 2;
   } else {
 
+  }
+  if (E_9 == 1) {
+    E_9 = 2;
+  } else {
+
   }
 
   return;
@@ -1078,6 +1183,7 @@ void activate_threads(void)
   int tmp___5 ;
   int tmp___6 ;
   int tmp___7 ;
+  int tmp___8 ;
 
   {
   {
@@ -1151,6 +1257,14 @@ void activate_threads(void)
     t8_st = 0;
   } else {
 
+  }
+  {
+  tmp___8 = is_transmit9_triggered();
+  }
+  if (tmp___8) {
+    t9_st = 0;
+  } else {
+
   }
 
   return;
@@ -1224,6 +1338,11 @@ void reset_time_events(void)
     T8_E = 2;
   } else {
 
+  }
+  if (T9_E == 1) {
+    T9_E = 2;
+  } else {
+
   }
   if (E_M == 1) {
     E_M = 2;
@@ -1269,6 +1388,11 @@ void reset_time_events(void)
     E_8 = 2;
   } else {
 
+  }
+  if (E_9 == 1) {
+    E_9 = 2;
+  } else {
+
   }
 
   return;
@@ -1287,6 +1411,7 @@ void init_model(void)
   t6_i = 1;
   t7_i = 1;
   t8_i = 1;
+  t9_i = 1;
 
   return;
 }
@@ -1326,7 +1451,7 @@ void start_simulation(void)
   }
   {
   while (1) {
-    while_10_continue: /* CIL Label */ ;
+    while_11_continue: /* CIL Label */ ;
     {
     kernel_st = 1;
     eval();
@@ -1358,12 +1483,12 @@ void start_simulation(void)
     tmp___0 = stop_simulation();
     }
     if (tmp___0) {
-      goto while_10_break;
+      goto while_11_break;
     } else {
 
     }
   }
-  while_10_break: /* CIL Label */ ;
+  while_11_break: /* CIL Label */ ;
   }
 
   return;
@@ -1382,4 +1507,4 @@ int _main(void)
 }
 }
 
-int main() {}
+int main() {}