Showing error 143

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_list.c-safe.cil.c
Line in file: 17
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 211 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h"
  5typedef unsigned long size_t;
  6#line 7 "files/rule60_list.c"
  7struct list_head {
  8   struct list_head *prev ;
  9   struct list_head *next ;
 10   int inserted ;
 11};
 12#line 2 "./assert.h"
 13void __blast_assert(void) 
 14{ 
 15
 16  {
 17  ERROR:assert(0); 
 18#line 4
 19  goto ERROR;
 20}
 21}
 22#line 51 "/usr/include/malloc.h"
 23extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 24#line 12 "files/rule60_list.c"
 25static void list_add(struct list_head *new , struct list_head *head ) 
 26{ int __cil_tmp3 ;
 27
Show full sources