Showing error 1367

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/fo_test.c_unsafe.cil.c
Line in file: 17
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/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h"
  5typedef unsigned long size_t;
  6#line 180 "/usr/include/bits/types.h"
  7typedef long __ssize_t;
  8#line 110 "/usr/include/sys/types.h"
  9typedef __ssize_t ssize_t;
 10#line 471 "/usr/include/stdlib.h"
 11extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 12#line 2 "./assert.h"
 13void __blast_assert(void) 
 14{ 
 15
 16  {
 17  ERROR: 
 18#line 4
 19  goto ERROR;
 20}
 21}
 22#line 87 "/usr/include/fcntl.h"
 23extern int open(char const   *__file , int __oflag  , ...)  __attribute__((__nonnull__(1))) ;
 24#line 8 "files/fo_test.c"
 25extern int __VERIFIER_nondet_int(void);
 26int open(char const   *__file, int __oflag, ...)  {
 27    int tmp =  __VERIFIER_nondet_int();
Show full sources
↑