typedef short Guard;
/* In order to be able to inspect the result... */
int res;
int T_res;
void square_root(int n)
{
{
/*TP*/ int T_n = n;
/*TP*/ Guard Ret = 0;
/*TP*/ Guard T_Ret = 0;
{
{
int result;
int T_result;
/* {char *CP0;} */
int k;
int T_k;
/* {char *CP1;} */
int i;
int T_i;
/* {char *CP2;} */
if (!Ret) i = 1;
if (!T_Ret) T_i = 1;
/* {char *CP3;} */
if (!Ret) result = 0;
if (!T_Ret) T_result = 0;
/* {char *CP4;} */
if (!Ret) k = 1;
if (!T_Ret) T_k = 1;
/* {char *CP5;} */
L1:;
T_L1:;
{
{
Guard G0 = 1;
Guard T_G0 = 1;
if (!Ret) G0 = (k <= n);
if (!T_Ret) T_G0 = (T_k <= T_n);
/* {char *CP6;} */
{
{
{
{
Guard G1 = 1;
Guard T_G1 = 1;
if (!Ret) if (G0) G1 = (k == n);
if (!T_Ret) if (T_G0) T_G1 = (T_k == T_n);
/* {char *CP7;} */
{
{
if (!Ret) if (G0) if (G1) result = i;
if (!T_Ret) if (T_G0) if (T_G1) T_result = T_i;
/* {char *CP8;} */
}
}
{
{
}
}
}
}
if (!Ret) if (G0) i = (i + 1);
if (!T_Ret) if (T_G0) T_i = (T_i + 1);
/* {char *CP9;} */
if (!Ret) if (G0) k = (i * i);
if (!T_Ret) if (T_G0) T_k = (T_i * T_i);
/* {char *CP10;} */
}
}
L2:;
T_L2:;
if (!Ret) if (G0) goto L1;
if (!T_Ret) if (T_G0) goto T_L1;
/* {char *CP11;} */
L3:;
T_L3:;
}
}
if (!Ret) res = result;
if (!T_Ret) T_res = T_result;
{char *CP12;}
}
}
}
}