Showing error 1411

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/structure_assignment.c_safe.cil.c
Line in file: 16
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 7 "files/structure_assignment.c"
 5struct Stuff {
 6   int a ;
 7   int b ;
 8};
 9#line 7 "files/structure_assignment.c"
10typedef struct Stuff Stuff;
11#line 2 "./assert.h"
12void __blast_assert(void) 
13{ 
14
15  {
16  ERROR: 
17#line 4
18  goto ERROR;
19}
20}
21#line 12 "files/structure_assignment.c"
22int main(void) 
23{ Stuff good ;
24  Stuff bad ;
25
26  {
27#line 14
28  good.a = 1;
29#line 14
30  good.b = 2;
31#line 16
32  bad = good;
33#line 17
34  if (bad.b == 2) {
35
36  } else {
37    {
38#line 17
39    __blast_assert();
40    }
41  }
42#line 18
43  return (0);
44}
45}
↑