Showing error 1201

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--rtc--rtc-r9701.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4701
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

4671  tmp___0 = __VERIFIER_nondet_int();
4672  }
4673#line 330
4674  if (tmp___0 != 0) {
4675#line 332
4676    goto ldv_23970;
4677  } else
4678#line 330
4679  if (ldv_s_r9701_driver_spi_driver != 0) {
4680#line 332
4681    goto ldv_23970;
4682  } else {
4683#line 334
4684    goto ldv_23972;
4685  }
4686  ldv_23972: ;
4687  ldv_module_exit: ;
4688  {
4689#line 444
4690  ldv_check_final_state();
4691  }
4692#line 447
4693  return;
4694}
4695}
4696#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2663/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4697void ldv_blast_assert(void) 
4698{ 
4699
4700  {
4701  ERROR: ;
4702#line 6
4703  goto ERROR;
4704}
4705}
4706#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2663/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4707extern int __VERIFIER_nondet_int(void) ;
4708#line 468 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2663/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-r9701.c.p"
4709int ldv_spin  =    0;
4710#line 472 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2663/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-r9701.c.p"
4711void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑