[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/token_ring.01_false.cil.c
[ 0:01] compiling /dios/lib/config/seqklee.bc
[ 0:01] setting up pass: functionmeta, options = 
[ 0:02] setting up pass: fuse-ctors, options = 
[ 0:02] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.18/_klee_out"
[ 0:03] KLEE: Using Z3 solver backend
[ 0:03] WARNING: this target does not support the llvm.stacksave intrinsic.
[ 0:03] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf'
[ 0:04] 
[ 0:04] KLEE: WARNING: undefined reference to function: __dios_tainted_init
[ 0:06] KLEE: WARNING: undefined reference to function: klee_free
[ 0:06] KLEE: WARNING: undefined reference to function: klee_malloc
[ 0:06] i:1
[ 0:06] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8.
[ 0:06] about to __boot:0
[ 0:06] about to run the scheduler:0
[ 0:06] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5
[ 0:06] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init
[ 0:06] KLEE: NOTE: now ignoring this error at this location
[ 0:06] KLEE: ERROR: EXITING ON ERROR:
[ 0:06] Error: failed external call: __dios_tainted_init
[ 0:06] File: /dios/libc/sys/start.cpp
[ 0:06] Line: 87
[ 0:06] assembly.ll line: 34811
[ 0:06] Stack: 
[ 0:06] 	#000034811 in __dios_start (l=0, argc=1, argv=94732946149896, envp=94732946219016) at /dios/libc/sys/start.cpp:87
[ 0:06] 	#100010830 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163
[ 0:06] 	#200043161 in klee_boot (argc=2, argv=94732919543808) at /dios/arch/klee/boot.c:41
[ 0:06] 
[ 0:06] 
[ 0:06]      1	/* TAGS: error c sym */
[ 0:06]      2	/* VERIFY_OPTS: --symbolic --sequential -o nofail:malloc */
[ 0:06]      3	extern void __VERIFIER_error() __attribute__ ((__noreturn__));
[ 0:06]      4	
[ 0:06]      5	/* Generated by CIL v. 1.3.6 */
[ 0:06]      6	/* print_CIL_Input is true */
[ 0:06]      7	
[ 0:06]      8	void error(void)
[ 0:06]      9	{
[ 0:06]     10	
[ 0:06]     11	  {
[ 0:06]     12	  ERROR: __VERIFIER_error(); /* ERROR */
[ 0:06]     13	  return;
[ 0:06]     14	}
[ 0:06]     15	}
[ 0:06]     16	int m_pc  =    0;
[ 0:06]     17	int t1_pc  =    0;
[ 0:06]     18	int m_st  ;
[ 0:06]     19	int t1_st  ;
[ 0:06]     20	int m_i  ;
[ 0:06]     21	int t1_i  ;
[ 0:06]     22	int M_E  =    2;
[ 0:06]     23	int T1_E  =    2;
[ 0:06]     24	int E_M  =    2;
[ 0:06]     25	int E_1  =    2;
[ 0:06]     26	int is_master_triggered(void) ;
[ 0:06]     27	int is_transmit1_triggered(void) ;
[ 0:06]     28	void immediate_notify(void) ;
[ 0:06]     29	int token  ;
[ 0:06]     30	int __VERIFIER_nondet_int()  ;
[ 0:06]     31	int local  ;
[ 0:06]     32	void master(void)
[ 0:06]     33	{
[ 0:06]     34	  int tmp_var = __VERIFIER_nondet_int();
[ 0:06]     35	  {
[ 0:06]     36	  if (m_pc == 0) {
[ 0:06]     37	    goto M_ENTRY;
[ 0:06]     38	  } else {
[ 0:06]     39	    if (m_pc == 1) {
[ 0:06]     40	      goto M_WAIT;
[ 0:06]     41	    } else {
[ 0:06]     42	
[ 0:06]     43	    }
[ 0:06]     44	  }
[ 0:06]     45	  M_ENTRY: ;
[ 0:06]     46	  {
[ 0:06]     47	  while (1) {
[ 0:06]     48	    while_0_continue: /* CIL Label */ ;
[ 0:06]     49	    {
[ 0:06]     50	    token = __VERIFIER_nondet_int();
[ 0:06]     51	    local = token;
[ 0:06]     52	    E_1 = 1;
[ 0:06]     53	    immediate_notify();
[ 0:06]     54	    E_1 = 2;
[ 0:06]     55	    m_pc = 1;
[ 0:06]     56	    m_st = 2;
[ 0:06]     57	    }
[ 0:06]     58	
[ 0:06]     59	    goto return_label;
[ 0:06]     60	    M_WAIT: ;
[ 0:06]     61	    if (token != local + 1) {
[ 0:06]     62	      {
[ 0:06]     63	      error();
[ 0:06]     64	      }
[ 0:06]     65	    } else {
[ 0:06]     66	       if(tmp_var <= 5){
[ 0:06]     67	           if(tmp_var >= 5){
[ 0:06]     68	
[ 0:06]     69	           }
[ 0:06]     70	        }
[ 0:06]     71	
[ 0:06]     72	        if(tmp_var <= 5){
[ 0:06]     73	           if(tmp_var >= 5){
[ 0:06]     74	             if(tmp_var == 5){
[ 0:06]     75	             error();
[ 0:06]     76	             }
[ 0:06]     77	          }
[ 0:06]     78	        }
[ 0:06]     79	    }
[ 0:06]     80	  }
[ 0:06]     81	  while_0_break: /* CIL Label */ ;
[ 0:06]     82	  }
[ 0:06]     83	
[ 0:06]     84	  return_label: /* CIL Label */
[ 0:06]     85	  return;
[ 0:06]     86	}
[ 0:06]     87	}
[ 0:06]     88	void transmit1(void)
[ 0:06]     89	{
[ 0:06]     90	
[ 0:06]     91	  {
[ 0:06]     92	  if (t1_pc == 0) {
[ 0:06]     93	    goto T1_ENTRY;
[ 0:06]     94	  } else {
[ 0:06]     95	    if (t1_pc == 1) {
[ 0:06]     96	      goto T1_WAIT;
[ 0:06]     97	    } else {
[ 0:06]     98	
[ 0:06]     99	    }
[ 0:06]    100	  }
[ 0:06]    101	  T1_ENTRY: ;
[ 0:06]    102	  {
[ 0:06]    103	  while (1) {
[ 0:06]    104	    while_1_continue: /* CIL Label */ ;
[ 0:06]    105	    t1_pc = 1;
[ 0:06]    106	    t1_st = 2;
[ 0:06]    107	
[ 0:06]    108	    goto return_label;
[ 0:06]    109	    T1_WAIT:
[ 0:06]    110	    {
[ 0:06]    111	    token += 1;
[ 0:06]    112	    E_M = 1;
[ 0:06]    113	    immediate_notify();
[ 0:06]    114	    E_M = 2;
[ 0:06]    115	    }
[ 0:06]    116	  }
[ 0:06]    117	  while_1_break: /* CIL Label */ ;
[ 0:06]    118	  }
[ 0:06]    119	
[ 0:06]    120	  return_label: /* CIL Label */
[ 0:06]    121	  return;
[ 0:06]    122	}
[ 0:06]    123	}
[ 0:06]    124	int is_master_triggered(void)
[ 0:06]    125	{ int __retres1 ;
[ 0:06]    126	
[ 0:06]    127	  {
[ 0:06]    128	  if (m_pc == 1) {
[ 0:06]    129	    if (E_M == 1) {
[ 0:06]    130	      __retres1 = 1;
[ 0:06]    131	      goto return_label;
[ 0:06]    132	    } else {
[ 0:06]    133	
[ 0:06]    134	    }
[ 0:06]    135	  } else {
[ 0:06]    136	
[ 0:06]    137	  }
[ 0:06]    138	  __retres1 = 0;
[ 0:06]    139	  return_label: /* CIL Label */
[ 0:06]    140	  return (__retres1);
[ 0:06]    141	}
[ 0:06]    142	}
[ 0:06]    143	int is_transmit1_triggered(void)
[ 0:06]    144	{ int __retres1 ;
[ 0:06]    145	
[ 0:06]    146	  {
[ 0:06]    147	  if (t1_pc == 1) {
[ 0:06]    148	    if (E_1 == 1) {
[ 0:06]    149	      __retres1 = 1;
[ 0:06]    150	      goto return_label;
[ 0:06]    151	    } else {
[ 0:06]    152	
[ 0:06]    153	    }
[ 0:06]    154	  } else {
[ 0:06]    155	
[ 0:06]    156	  }
[ 0:06]    157	  __retres1 = 0;
[ 0:06]    158	  return_label: /* CIL Label */
[ 0:06]    159	  return (__retres1);
[ 0:06]    160	}
[ 0:06]    161	}
[ 0:06]    162	void update_channels(void)
[ 0:06]    163	{
[ 0:06]    164	
[ 0:06]    165	  {
[ 0:06]    166	
[ 0:06]    167	  return;
[ 0:06]    168	}
[ 0:06]    169	}
[ 0:06]    170	void init_threads(void)
[ 0:06]    171	{
[ 0:06]    172	
[ 0:06]    173	  {
[ 0:06]    174	  if (m_i == 1) {
[ 0:06]    175	    m_st = 0;
[ 0:06]    176	  } else {
[ 0:06]    177	    m_st = 2;
[ 0:06]    178	  }
[ 0:06]    179	  if (t1_i == 1) {
[ 0:06]    180	    t1_st = 0;
[ 0:06]    181	  } else {
[ 0:06]    182	    t1_st = 2;
[ 0:06]    183	  }
[ 0:06]    184	
[ 0:06]    185	  return;
[ 0:06]    186	}
[ 0:06]    187	}
[ 0:06]    188	int exists_runnable_thread(void)
[ 0:06]    189	{ int __retres1 ;
[ 0:06]    190	
[ 0:06]    191	  {
[ 0:06]    192	  if (m_st == 0) {
[ 0:06]    193	    __retres1 = 1;
[ 0:06]    194	    goto return_label;
[ 0:06]    195	  } else {
[ 0:06]    196	    if (t1_st == 0) {
[ 0:06]    197	      __retres1 = 1;
[ 0:06]    198	      goto return_label;
[ 0:06]    199	    } else {
[ 0:06]    200	
[ 0:06]    201	    }
[ 0:06]    202	  }
[ 0:06]    203	  __retres1 = 0;
[ 0:06]    204	  return_label: /* CIL Label */
[ 0:06]    205	  return (__retres1);
[ 0:06]    206	}
[ 0:06]    207	}
[ 0:06]    208	void eval(void)
[ 0:06]    209	{
[ 0:06]    210	  int tmp ;
[ 0:06]    211	
[ 0:06]    212	  {
[ 0:06]    213	  {
[ 0:06]    214	  while (1) {
[ 0:06]    215	    while_2_continue: /* CIL Label */ ;
[ 0:06]    216	    {
[ 0:06]    217	    tmp = exists_runnable_thread();
[ 0:06]    218	    }
[ 0:06]    219	    if (tmp) {
[ 0:06]    220	
[ 0:06]    221	    } else {
[ 0:06]    222	      goto while_2_break;
[ 0:06]    223	    }
[ 0:06]    224	    if (m_st == 0) {
[ 0:06]    225	      int tmp_ndt_1;
[ 0:06]    226	      tmp_ndt_1 = __VERIFIER_nondet_int();
[ 0:06]    227	      if (tmp_ndt_1) {
[ 0:06]    228	        {
[ 0:06]    229	        m_st = 1;
[ 0:06]    230	        master();
[ 0:06]    231	        }
[ 0:06]    232	      } else {
[ 0:06]    233	
[ 0:06]    234	      }
[ 0:06]    235	    } else {
[ 0:06]    236	
[ 0:06]    237	    }
[ 0:06]    238	    if (t1_st == 0) {
[ 0:06]    239	      int tmp_ndt_2;
[ 0:06]    240	      tmp_ndt_2 = __VERIFIER_nondet_int();
[ 0:06]    241	      if (tmp_ndt_2) {
[ 0:06]    242	        {
[ 0:06]    243	        t1_st = 1;
[ 0:06]    244	        transmit1();
[ 0:06]    245	        }
[ 0:06]    246	      } else {
[ 0:06]    247	
[ 0:06]    248	      }
[ 0:06]    249	    } else {
[ 0:06]    250	
[ 0:06]    251	    }
[ 0:06]    252	  }
[ 0:06]    253	  while_2_break: /* CIL Label */ ;
[ 0:06]    254	  }
[ 0:06]    255	
[ 0:06]    256	  return;
[ 0:06]    257	}
[ 0:06]    258	}
[ 0:06]    259	void fire_delta_events(void)
[ 0:06]    260	{
[ 0:06]    261	
[ 0:06]    262	  {
[ 0:06]    263	  if (M_E == 0) {
[ 0:06]    264	    M_E = 1;
[ 0:06]    265	  } else {
[ 0:06]    266	
[ 0:06]    267	  }
[ 0:06]    268	  if (T1_E == 0) {
[ 0:06]    269	    T1_E = 1;
[ 0:06]    270	  } else {
[ 0:06]    271	
[ 0:06]    272	  }
[ 0:06]    273	  if (E_M == 0) {
[ 0:06]    274	    E_M = 1;
[ 0:06]    275	  } else {
[ 0:06]    276	
[ 0:06]    277	  }
[ 0:06]    278	  if (E_1 == 0) {
[ 0:06]    279	    E_1 = 1;
[ 0:06]    280	  } else {
[ 0:06]    281	
[ 0:06]    282	  }
[ 0:06]    283	
[ 0:06]    284	  return;
[ 0:06]    285	}
[ 0:06]    286	}
[ 0:06]    287	void reset_delta_events(void)
[ 0:06]    288	{
[ 0:06]    289	
[ 0:06]    290	  {
[ 0:06]    291	  if (M_E == 1) {
[ 0:06]    292	    M_E = 2;
[ 0:06]    293	  } else {
[ 0:06]    294	
[ 0:06]    295	  }
[ 0:06]    296	  if (T1_E == 1) {
[ 0:06]    297	    T1_E = 2;
[ 0:06]    298	  } else {
[ 0:06]    299	
[ 0:06]    300	  }
[ 0:06]    301	  if (E_M == 1) {
[ 0:06]    302	    E_M = 2;
[ 0:06]    303	  } else {
[ 0:06]    304	
[ 0:06]    305	  }
[ 0:06]    306	  if (E_1 == 1) {
[ 0:06]    307	    E_1 = 2;
[ 0:06]    308	  } else {
[ 0:06]    309	
[ 0:06]    310	  }
[ 0:06]    311	
[ 0:06]    312	  return;
[ 0:06]    313	}
[ 0:06]    314	}
[ 0:06]    315	void activate_threads(void)
[ 0:06]    316	{ int tmp ;
[ 0:06]    317	  int tmp___0 ;
[ 0:06]    318	
[ 0:06]    319	  {
[ 0:06]    320	  {
[ 0:06]    321	  tmp = is_master_triggered();
[ 0:06]    322	  }
[ 0:06]    323	  if (tmp) {
[ 0:06]    324	    m_st = 0;
[ 0:06]    325	  } else {
[ 0:06]    326	
[ 0:06]    327	  }
[ 0:06]    328	  {
[ 0:06]    329	  tmp___0 = is_transmit1_triggered();
[ 0:06]    330	  }
[ 0:06]    331	  if (tmp___0) {
[ 0:06]    332	    t1_st = 0;
[ 0:06]    333	  } else {
[ 0:06]    334	
[ 0:06]    335	  }
[ 0:06]    336	
[ 0:06]    337	  return;
[ 0:06]    338	}
[ 0:06]    339	}
[ 0:06]    340	void immediate_notify(void)
[ 0:06]    341	{
[ 0:06]    342	
[ 0:06]    343	  {
[ 0:06]    344	  {
[ 0:06]    345	  activate_threads();
[ 0:06]    346	  }
[ 0:06]    347	
[ 0:06]    348	  return;
[ 0:06]    349	}
[ 0:06]    350	}
[ 0:06]    351	void fire_time_events(void)
[ 0:06]    352	{
[ 0:06]    353	
[ 0:06]    354	  {
[ 0:06]    355	  M_E = 1;
[ 0:06]    356	
[ 0:06]    357	  return;
[ 0:06]    358	}
[ 0:06]    359	}
[ 0:06]    360	void reset_time_events(void)
[ 0:06]    361	{
[ 0:06]    362	
[ 0:06]    363	  {
[ 0:06]    364	  if (M_E == 1) {
[ 0:06]    365	    M_E = 2;
[ 0:06]    366	  } else {
[ 0:06]    367	
[ 0:06]    368	  }
[ 0:06]    369	  if (T1_E == 1) {
[ 0:06]    370	    T1_E = 2;
[ 0:06]    371	  } else {
[ 0:06]    372	
[ 0:06]    373	  }
[ 0:06]    374	  if (E_M == 1) {
[ 0:06]    375	    E_M = 2;
[ 0:06]    376	  } else {
[ 0:06]    377	
[ 0:06]    378	  }
[ 0:06]    379	  if (E_1 == 1) {
[ 0:06]    380	    E_1 = 2;
[ 0:06]    381	  } else {
[ 0:06]    382	
[ 0:06]    383	  }
[ 0:06]    384	
[ 0:06]    385	  return;
[ 0:06]    386	}
[ 0:06]    387	}
[ 0:06]    388	void init_model(void)
[ 0:06]    389	{
[ 0:06]    390	
[ 0:06]    391	  {
[ 0:06]    392	  m_i = 1;
[ 0:06]    393	  t1_i = 1;
[ 0:06]    394	
[ 0:06]    395	  return;
[ 0:06]    396	}
[ 0:06]    397	}
[ 0:06]    398	int stop_simulation(void)
[ 0:06]    399	{ int tmp ;
[ 0:06]    400	  int __retres2 ;
[ 0:06]    401	
[ 0:06]    402	  {
[ 0:06]    403	  {
[ 0:06]    404	  tmp = exists_runnable_thread();
[ 0:06]    405	  }
[ 0:06]    406	  if (tmp) {
[ 0:06]    407	    __retres2 = 0;
[ 0:06]    408	    goto return_label;
[ 0:06]    409	  } else {
[ 0:06]    410	
[ 0:06]    411	  }
[ 0:06]    412	  __retres2 = 1;
[ 0:06]    413	  return_label: /* CIL Label */
[ 0:06]    414	  return (__retres2);
[ 0:06]    415	}
[ 0:06]    416	}
[ 0:06]    417	void start_simulation(void)
[ 0:06]    418	{ int kernel_st ;
[ 0:06]    419	  int tmp ;
[ 0:06]    420	  int tmp___0 ;
[ 0:06]    421	
[ 0:06]    422	  {
[ 0:06]    423	  {
[ 0:06]    424	  kernel_st = 0;
[ 0:06]    425	  update_channels();
[ 0:06]    426	  init_threads();
[ 0:06]    427	  fire_delta_events();
[ 0:06]    428	  activate_threads();
[ 0:06]    429	  reset_delta_events();
[ 0:06]    430	  }
[ 0:06]    431	  {
[ 0:06]    432	  while (1) {
[ 0:06]    433	    while_3_continue: /* CIL Label */ ;
[ 0:06]    434	    {
[ 0:06]    435	    kernel_st = 1;
[ 0:06]    436	    eval();
[ 0:06]    437	    }
[ 0:06]    438	    {
[ 0:06]    439	    kernel_st = 2;
[ 0:06]    440	    update_channels();
[ 0:06]    441	    }
[ 0:06]    442	    {
[ 0:06]    443	    kernel_st = 3;
[ 0:06]    444	    fire_delta_events();
[ 0:06]    445	    activate_threads();
[ 0:06]    446	    reset_delta_events();
[ 0:06]    447	    }
[ 0:06]    448	    {
[ 0:06]    449	    tmp = exists_runnable_thread();
[ 0:06]    450	    }
[ 0:06]    451	    if (tmp == 0) {
[ 0:06]    452	      {
[ 0:06]    453	      kernel_st = 4;
[ 0:06]    454	      fire_time_events();
[ 0:06]    455	      activate_threads();
[ 0:06]    456	      reset_time_events();
[ 0:06]    457	      }
[ 0:06]    458	    } else {
[ 0:06]    459	
[ 0:06]    460	    }
[ 0:06]    461	    {
[ 0:06]    462	    tmp___0 = stop_simulation();
[ 0:06]    463	    }
[ 0:06]    464	    if (tmp___0) {
[ 0:06]    465	      goto while_3_break;
[ 0:06]    466	    } else {
[ 0:06]    467	
[ 0:06]    468	    }
[ 0:06]    469	  }
[ 0:06]    470	  while_3_break: /* CIL Label */ ;
[ 0:06]    471	  }
[ 0:06]    472	
[ 0:06]    473	  return;
[ 0:06]    474	}
[ 0:06]    475	}
[ 0:06]    476	int main(void)
[ 0:06]    477	{ int __retres1 ;
[ 0:06]    478	
[ 0:06]    479	  {
[ 0:06]    480	  {
[ 0:06]    481	  init_model();
[ 0:06]    482	  start_simulation();
[ 0:06]    483	  }
[ 0:06]    484	  __retres1 = 0;
[ 0:06]    485	  return (__retres1);
[ 0:06]    486	}
[ 0:06]    487	}
[ 0:06] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/token_ring.01_false.cil.c:12, but it was not