Showing error 1412

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.i
Line in file: 12
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 1# 1 "files/structure_assignment.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/structure_assignment.c"
 5
 6
 7
 8# 1 "./assert.h" 1
 9
10void __blast_assert()
11{
12 ERROR: goto ERROR;
13}
14# 5 "files/structure_assignment.c" 2
15
16
17
18typedef struct Stuff {
19 int a;
20 int b;
21} Stuff;
22
23int main()
24{
25 Stuff good = {1,2};
26 Stuff bad;
27 bad = good;
28 ((bad.b == 2) ? (0) : __blast_assert ());
29 return 0;
30}
↑