5 files changed, 33 insertions, 0 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v
index a1c1d9cb..1b3d415d 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -1,3 +1,9 @@
+(*
+Replace available expressions by the register containing their value.
+
+David Monniaux, CNRS, VERIMAG
+ *)
+
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Memory Registers Op RTL Maps.
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index f0351c3a..2b9b71dc 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1,3 +1,11 @@
+(*
+Replace available expressions by the register containing their value.
+
+Proofs.
+
+David Monniaux, CNRS, VERIMAG
+ *)
+
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Memory Registers Op RTL Maps.
diff --git a/test/monniaux/cse2/loopaccess.c b/test/monniaux/cse2/loopaccess.c
new file mode 100644
index 00000000..5ddaeb66
--- /dev/null
+++ b/test/monniaux/cse2/loopaccess.c
@@ -0,0 +1,7 @@
+double toto(double x, int count) {
+  double r = 5*x + 3;
+  while (count > r) {
+    count --;
+  }
+  return 5*x + 3;
+}
diff --git a/test/monniaux/cse2/loopinvariant.c b/test/monniaux/cse2/loopinvariant.c
new file mode 100644
index 00000000..64caf80b
--- /dev/null
+++ b/test/monniaux/cse2/loopinvariant.c
@@ -0,0 +1,7 @@
+int toto(int *t, int n) {
+  int x = t[0];
+  for(int i=1; i<n; i++) {
+    if (t[i] > t[0]) return i;
+  }
+  return 0;
+}
diff --git a/test/monniaux/cse2/loopload.c b/test/monniaux/cse2/loopload.c
new file mode 100644
index 00000000..6e0925f7
--- /dev/null
+++ b/test/monniaux/cse2/loopload.c
@@ -0,0 +1,5 @@
+int find_index(int *t, int n) {
+  if (t[0] > 0) return 3;
+  while (n > 0) n--;
+  return t[0];
+}