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
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
typedef short Guard;

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

void gcd(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;} */
{
{
Guard G0 = 1;
Guard T_G0 = 1;
if (!Ret) G0 = ((1 <= a) && (1 <= b));
if (!T_Ret) T_G0 = ((1 <= T_a) && (1 <= T_b));
/* {char *CP1;} */
{
{
L1:;
T_L1:;
{
{
Guard G1 = 1;
Guard T_G1 = 1;
if (!Ret) if (G0) G1 = (!(a == b));
if (!T_Ret) if (T_G0) T_G1 = (!(T_a == T_b));
/* {char *CP2;} */
{
{
{
{
Guard G2 = 1;
Guard T_G2 = 1;
if (!Ret) if (G0) if (G1) G2 = (a <= b);
if (!T_Ret) if (T_G0) if (T_G1) T_G2 = (T_a <= T_b);
/* {char *CP3;} */
{
{
if (!Ret) if (G0) if (G1) if (G2) b = (b - a);
if (!T_Ret) if (T_G0) if (T_G1) if (T_G2) T_b = (T_b - T_a);
/* {char *CP4;} */
}
}
{
{
if (!Ret) if (G0) if (G1) if (!G2) a = (a - b);
if (!T_Ret) if (T_G0) if (T_G1) if (!T_G2) T_a = (T_a - T_b);
/* {char *CP5;} */
}
}
}
}
{
Guard T_G3 = 1;
if (!T_Ret) if (T_G0) if (T_G1) T_G3 = (!(T_a == T_b));
{
{
Guard T_G4 = 1;
if (!T_Ret) if (T_G0) if (T_G1) if (T_G3) T_G4 = (T_a <= T_b);
{
if (!T_Ret) if (T_G0) if (T_G1) if (T_G3) if (T_G4) T_b = (T_b - T_a);
/* {char *CP6;} */
}
}
{
if (!T_Ret) if (T_G0) if (T_G1) if (T_G3) if (!T_G4) T_a = (T_a - T_b);
}
}
}
{
}
}
}
/* {char *CP7;} */
L2:;
T_L2:;
if (!Ret) if (G0) if (G1) goto L1;
if (!T_Ret) if (T_G0) if (T_G1) goto T_L1;
/* {char *CP8;} */
L3:;
T_L3:;
}
}
if (!Ret) if (G0) result = a;
if (!T_Ret) if (T_G0) T_result = T_a;
/* {char *CP9;} */
}
}
{
{
if (!Ret) if (!G0) result = 0;
if (!T_Ret) if (!T_G0) T_result = 0;
/* {char *CP10;} */
}
}
}
}
if (!Ret) res = result;
if (!T_Ret) T_res = T_result;
{char *CP11;}
}
}
}
}