Showing error 1405

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/rule60_list2.c_unsafe_1.cil.c
Line in file: 14
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 29 "files/rule60_list2.c"
  5struct list_head {
  6   struct list_head *prev ;
  7   struct list_head *next ;
  8};
  9#line 2 "./assert.h"
 10void __blast_assert(void) 
 11{ 
 12
 13  {
 14  ERROR: 
 15#line 4
 16  goto ERROR;
 17}
 18}
 19#line 11 "files/rule60_list2.c"
 20extern int __VERIFIER_nondet_int(void) ;
 21#line 13 "files/rule60_list2.c"
 22void *guard_malloc_counter  =    (void *)0;
 23#line 15 "files/rule60_list2.c"
 24void *__getMemory(int size )
Show full sources
↑