Showing error 1262

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--usb--atm--xusbatm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 8072
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

8042    goto ldv_40870;
8043  } else
8044#line 337
8045  if (ldv_s_xusbatm_usb_driver_usb_driver != 0) {
8046#line 339
8047    goto ldv_40870;
8048  } else {
8049#line 341
8050    goto ldv_40872;
8051  }
8052  ldv_40872: ;
8053  ldv_module_exit: 
8054  {
8055#line 388
8056  xusbatm_exit();
8057  }
8058  ldv_final: 
8059  {
8060#line 391
8061  ldv_check_final_state();
8062  }
8063#line 394
8064  return;
8065}
8066}
8067#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2039/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8068void ldv_blast_assert(void) 
8069{ 
8070
8071  {
8072  ERROR: ;
8073#line 6
8074  goto ERROR;
8075}
8076}
8077#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2039/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8078extern int __VERIFIER_nondet_int(void) ;
8079#line 415 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2039/dscv_tempdir/dscv/ri/43_1a/drivers/usb/atm/xusbatm.c.p"
8080int ldv_spin  =    0;
8081#line 419 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2039/dscv_tempdir/dscv/ri/43_1a/drivers/usb/atm/xusbatm.c.p"
8082void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑