Showing error 1350

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_unsafe_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 7360
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 7330#line 503
 7331        tmp___3 = (char *)"SEND";
 7332      } else {
 7333#line 503
 7334        tmp___3 = (char *)"RECV";
 7335      }
 7336      {
 7337#line 503
 7338      __cil_tmp101 = (unsigned long )udc;
 7339#line 503
 7340      __cil_tmp102 = __cil_tmp101 + 1296;
 7341#line 503
 7342      __cil_tmp103 = *((struct platform_device **)__cil_tmp102);
 7343#line 503
 7344      __cil_tmp104 = (unsigned long )__cil_tmp103;
 7345#line 503
 7346      __cil_tmp105 = __cil_tmp104 + 16;
 7347#line 503
 7348      __cil_tmp106 = (struct device *)__cil_tmp105;
 7349#line 503
 7350      __cil_tmp107 = (struct device    *)__cil_tmp106;
 7351#line 503
 7352      __cil_tmp108 = (unsigned long )ep;
 7353#line 503
 7354      __cil_tmp109 = __cil_tmp108 + 123;
 7355#line 503
 7356      __cil_tmp110 = *((unsigned char *)__cil_tmp109);
 7357#line 503
 7358      __cil_tmp111 = (unsigned int )__cil_tmp110;
 7359#line 503
 7360      _dev_info(__cil_tmp107, "ep=%d %s: Init ERROR: ENDPTPRIME=0x%x, ENDPTSTATUS=0x%x, bit_pos=0x%x\n",
 7361                __cil_tmp111, tmp___3, tmp___2, tmp___1, bit_pos);
 7362      }
 7363#line 510
 7364      goto en_done;
 7365    } else {
 7366
 7367    }
 7368    }
 7369  }
 7370  }
Show full sources
↑