1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
typedef short Guard;

/* In order to be able to inspect the result... */
int res;
int T_res;

void twoloops(int a, int b)
{
{
/*TP*/ int T_a = a;
/*TP*/ int T_b = b;
/*TP*/ Guard Ret = 0;
/*TP*/ Guard T_Ret = 0;
{
{
int result;
int T_result;
/* {char *CP0;} */
int b10;
int T_b10;
/* {char *CP1;} */
int a10;
int T_a10;
/* {char *CP2;} */
if (!Ret) a10 = 0;
if (!T_Ret) T_a10 = 0;
/* {char *CP3;} */
if (!Ret) b10 = 0;
if (!T_Ret) T_b10 = 0;
/* {char *CP4;} */
L1:;
T_L1:;
{
{
Guard G0 = 1;
Guard T_G0 = 1;
if (!T_Ret) T_G0 = (10 <= T_b);
if (!Ret) G0 = (10 <= a);
/* {char *CP5;} */
{
{
if (!T_Ret) if (T_G0) T_b10 = (T_b10 + 1);
if (!T_Ret) if (T_G0) T_b = (T_b - 10);
if (!Ret) if (G0) a10 = (a10 + 1);
if (!Ret) if (G0) a = (a - 10);
/* {char *CP6;} */
}
}
L2:;
T_L2:;
if (!Ret) if (G0) goto L1;
if (!T_Ret) if (T_G0) goto T_L1;
/* {char *CP7;} */
L3:;
T_L3:;
}
}
L4:;
T_L4:;
{
{
Guard G1 = 1;
Guard T_G1 = 1;
if (!T_Ret) T_G1 = (10 <= T_a);
if (!Ret) G1 = (10 <= b);
/* {char *CP8;} */
{
{
if (!T_Ret) if (T_G1) T_a10 = (T_a10 + 1);
if (!T_Ret) if (T_G1) T_a = (T_a - 10);
if (!Ret) if (G1) b10 = (b10 + 1);
if (!Ret) if (G1) b = (b - 10);
/* {char *CP9;} */
}
}
L5:;
T_L5:;
if (!Ret) if (G1) goto L4;
if (!T_Ret) if (T_G1) goto T_L4;
/* {char *CP10;} */
L6:;
T_L6:;
}
}
if (!Ret) result = ((a10 + b10) * 10);
if (!T_Ret) T_result = ((T_a10 + T_b10) * 10);
/* {char *CP11;} */
if (!Ret) res = result;
if (!T_Ret) T_res = T_result;
{char *CP12;}
}
}
}
}