summaryrefslogtreecommitdiff
path: root/test/cminor
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-18 15:52:24 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-18 15:52:24 +0000
commit165407527b1be7df6a376791719321c788e55149 (patch)
tree35c2eb9603f007b033fced56f21fa49fd105562f /test/cminor
parent1346309fd03e19da52156a700d037c348f27af0d (diff)
Simplification de Cminor: les affectations de variables locales ne sont
plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/cminor')
-rw-r--r--test/cminor/aes.cmp15
1 files changed, 10 insertions, 5 deletions
diff --git a/test/cminor/aes.cmp b/test/cminor/aes.cmp
index 35eabc4..11a253c 100644
--- a/test/cminor/aes.cmp
+++ b/test/cminor/aes.cmp
@@ -42,7 +42,8 @@
rk(5) = rk(1) ^ rk(4);
rk(6) = rk(2) ^ rk(5);
rk(7) = rk(3) ^ rk(6);
- if ((i = i + 1) == 10) {
+ i = i + 1;
+ if (i == 10) {
return 10;
}
rk_ = rk_ + 4 * 4;
@@ -62,7 +63,8 @@
rk( 7) = rk( 1) ^ rk( 6);
rk( 8) = rk( 2) ^ rk( 7);
rk( 9) = rk( 3) ^ rk( 8);
- if ((i = i + 1) == 8) {
+ i = i + 1;
+ if (i == 8) {
return 12;
}
rk(10) = rk( 4) ^ rk( 9);
@@ -84,7 +86,8 @@
rk( 9) = rk( 1) ^ rk( 8);
rk(10) = rk( 2) ^ rk( 9);
rk(11) = rk( 3) ^ rk(10);
- if ((i = i + 1) == 7) {
+ i = i + 1;
+ if (i == 7) {
return 14;
}
temp = rk(11);
@@ -198,7 +201,8 @@
rk(7);
rk_ = rk_ + 8 * 4;
- if ((r = r - 1) == 0) exit;
+ r = r - 1;
+ if (r == 0) exit;
s0 =
Te0((t0 >>u 24) ) ^
@@ -302,7 +306,8 @@
rk(7);
rk_ = rk_ + 8 * 4;
- if ((r = r - 1) == 0) exit;
+ r = r - 1;
+ if (r == 0) exit;
s0 =
Td0((t0 >>u 24) ) ^