Showing error 59

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: heap-manipulation/merge_sort_unsafe.cil.c
Line in file: 29
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 211 "/usr/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
  5typedef unsigned int size_t;
  6#line 15 "test-0178.c"
  7struct node {
  8   struct node *next ;
  9   int value ;
 10};
 11#line 20 "test-0178.c"
 12struct list {
 13   struct node *slist ;
 14   struct list *next ;
 15};
 16#line 471 "/usr/include/stdlib.h"
 17extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 18#line 488
 19extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
 20#line 514
 21extern  __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
 22#line 3 "test-0178.c"
 23extern int __VERIFIER_nondet_int(void) ;
 24#line 5 "test-0178.c"
 25static void fail(void) 
 26{ 
 27
 28  {
 29  ERROR: 
 30  goto ERROR;
 31}
 32}
 33#line 25 "test-0178.c"
 34static void merge_single_node(struct node ***dst , struct node **data ) 
 35{ struct node *node ;
 36  void *__cil_tmp4 ;
 37  struct node **__cil_tmp5 ;
 38
 39  {
Show full sources
↑