Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2

3 files changed, 19 insertions, 0 deletions

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];
+}