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 ) 
26{ int retVal ;
27  ssize_t tmp ;
28  unsigned int __cil_tmp5 ;
29  char const   * __restrict  __cil_tmp6 ;
30
31  {
32  {
33#line 13
34  tmp = getService();
35#line 13
36  retVal = (int )tmp;
37  }
38  {
39#line 14
40  __cil_tmp5 = (unsigned int )globalSize;
41#line 14
42  if (4U == __cil_tmp5) {
43
44  } else {
45    {
46#line 14
47    __blast_assert();
48    }
49  }
50  }
51  {
52#line 15
53  __cil_tmp6 = (char const   * __restrict  )"returned value: %d\n";
54#line 15
55  printf(__cil_tmp6, retVal);
56  }
57#line 16
58  return (0);
59}
60}
61#line 20 "files/test_overflow.c"
62ssize_t getService(void) 
63{ ssize_t localVar ;
64  char const   * __restrict  __cil_tmp2 ;
65
66  {
67  {
68#line 21
69  localVar = (ssize_t )999999999999LL;
70#line 22
71  globalSize = (int )4U;
72#line 23
73  __cil_tmp2 = (char const   * __restrict  )"localVar: %d\n";
74#line 23
75  printf(__cil_tmp2, localVar);
76  }
77#line 24
78  return (localVar);
79}
80}
↑