Showing error 153

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/test_overflow.c-safe.cil.c
Line in file: 15
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 180 "/usr/include/bits/types.h"
 5typedef long __ssize_t;
 6#line 110 "/usr/include/sys/types.h"
 7typedef __ssize_t ssize_t;
 8#line 341 "/usr/include/stdio.h"
 9extern int printf(char const   * __restrict  __format  , ...) ;
10#line 2 "./assert.h"
11void __blast_assert(void) 
12{ 
13
14  {
15  ERROR:assert(0); 
16#line 4
17  goto ERROR;
18}
19}
20#line 7 "files/test_overflow.c"
21ssize_t getService(void) ;
22#line 8 "files/test_overflow.c"
23int globalSize  ;
24#line 10 "files/test_overflow.c"
25int main(int argc , char **argv ) 
Show full sources