Showing error 164

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/1_3.c-unsafe.cil.c
Line in file: 19
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/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
  5typedef unsigned int size_t;
  6#line 3 "files/1_3.h"
  7struct RR {
  8   int state ;
  9};
 10#line 8 "files/1_3.h"
 11typedef struct RR rr;
 12#line 471 "/usr/include/stdlib.h"
 13extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 14#line 2 "./assert.h"
 15void __blast_assert(void) 
 16{ 
 17
 18  {
 19  ERROR:assert(0); 
 20#line 4
 21  goto ERROR;
 22}
 23}
 24#line 10 "files/1_3.h"
 25extern void *__VERIFIER_nondet_pointer() ;
 26#line 23 "files/1_3.c"
 27rr *getrr(void) 
 28{ rr *r ;
 29  void *tmp ;
Show full sources
↑