From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 28 Aug 2007 12:57:58 +0000
Subject: Fusion de la branche restr-cminor.  En Clight, C#minor et Cminor, les
 expressions sont maintenant pures et les appels de fonctions sont des
 statements.  Ajout de semantiques coinductives pour la divergence en Clight,
 C#minor, Cminor.  Preuve de preservation semantique pour les programmes qui
 divergent.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 test/c/Results/lists | 1 +
 test/cminor/sha1.cmp | 6 ++++--
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'test')

diff --git a/test/c/Results/lists b/test/c/Results/lists
index d86bac9d..2c94e483 100644
--- a/test/c/Results/lists
+++ b/test/c/Results/lists
@@ -1 +1,2 @@
 OK
+OK
diff --git a/test/cminor/sha1.cmp b/test/cminor/sha1.cmp
index 31c4b178..9d7744c5 100644
--- a/test/cminor/sha1.cmp
+++ b/test/cminor/sha1.cmp
@@ -125,11 +125,13 @@ extern "memset" : int -> int -> int -> void
 
 "SHA1_add_data"(ctx, data, len) : int -> int -> int -> void
 {
-  var t;
+  var t, t2;
 
   /* Update length */
   t = context_length_lo(ctx);
-  if ((context_length_lo(ctx) = t + (len << 3)) <u t)
+  t2 = t + (len << 3);
+  context_length_lo(ctx) = t2;
+  if (t2 <u t)
     context_length_hi(ctx) = context_length_hi(ctx) + 1;
   context_length_hi(ctx) = context_length_hi(ctx) + (len >>u 29);
 
-- 
cgit