Showing error 1268

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

Source: 

5481    goto ldv_24301;
5482  } else
5483#line 791
5484  if (ldv_s_ab8500_usb_driver_platform_driver != 0) {
5485#line 793
5486    goto ldv_24301;
5487  } else {
5488#line 795
5489    goto ldv_24303;
5490  }
5491  ldv_24303: ;
5492  ldv_module_exit: 
5493  {
5494#line 961
5495  ab8500_usb_exit();
5496  }
5497  ldv_final: 
5498  {
5499#line 964
5500  ldv_check_final_state();
5501  }
5502#line 967
5503  return;
5504}
5505}
5506#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1864/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5507void ldv_blast_assert(void) 
5508{ 
5509
5510  {
5511  ERROR: ;
5512#line 6
5513  goto ERROR;
5514}
5515}
5516#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1864/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5517extern int __VERIFIER_nondet_int(void) ;
5518#line 988 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1864/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/ab8500-usb.c.p"
5519int ldv_spin  =    0;
5520#line 992 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1864/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/ab8500-usb.c.p"
5521void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑