Showing error 770

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


Source:

1096  unsigned int __cil_tmp19 ;
1097
1098  {
1099  {
1100#line 146
1101  ret = -22;
1102#line 148
1103  __cil_tmp3 = & ks0108_port;
1104#line 148
1105  __cil_tmp4 = *__cil_tmp3;
1106#line 148
1107  __cil_tmp5 = (unsigned long )__cil_tmp4;
1108#line 148
1109  ks0108_parport = parport_find_base(__cil_tmp5);
1110  }
1111  {
1112#line 149
1113  __cil_tmp6 = (struct parport *)0;
1114#line 149
1115  __cil_tmp7 = (unsigned long )__cil_tmp6;
1116#line 149
1117  __cil_tmp8 = (unsigned long )ks0108_parport;
1118#line 149
1119  if (__cil_tmp8 == __cil_tmp7) {
1120    {
1121#line 150
1122    __cil_tmp9 = & ks0108_port;
1123#line 150
1124    __cil_tmp10 = *__cil_tmp9;
1125#line 150
1126    printk("<3>ks0108: ERROR: parport didn\'t find %i port\n", __cil_tmp10);
1127    }
1128#line 152
1129    goto none;
1130  } else {
1131
1132  }
1133  }
1134  {
1135#line 155
1136  __cil_tmp11 = (int (*)(void * ))0;
Show full sources