Showing error 141

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/rule57_ebda_blast.c-safe_1.cil.c
Line in file: 29
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 10 "files/rule57_ebda_blast.c"
  5struct hotplug_slot;
  6#line 10
  7struct hotplug_slot;
  8#line 12 "files/rule57_ebda_blast.c"
  9struct bus_info {
 10
 11};
 12#line 15 "files/rule57_ebda_blast.c"
 13struct slot {
 14   int a ;
 15   int b ;
 16   struct hotplug_slot *hotplug_slot ;
 17   struct bus_info *bus_on ;
 18};
 19#line 22 "files/rule57_ebda_blast.c"
 20struct hotplug_slot {
 21   struct slot *private ;
 22   int b ;
 23};
 24#line 2 "./assert.h"
 25void __blast_assert(void) 
 26{ 
 27
 28  {
 29  ERROR:assert(0); 
 30#line 4
 31  goto ERROR;
 32}
 33}
 34#line 32 "files/rule57_ebda_blast.c"
 35struct slot *tmp_slot  ;
 36#line 33 "files/rule57_ebda_blast.c"
 37int used_tmp_slot  =    0;
 38#line 34 "files/rule57_ebda_blast.c"
 39int freed_tmp_slot  =    1;
Show full sources
↑