aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/cse2
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-20 14:06:21 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-20 14:06:21 +0200
commit168393089024b5f926836cb813fddf14e6b6e4d4 (patch)
tree5d018198dc26be847544f162b87ad3dcecbab479 /test/monniaux/cse2
parent633b72565b022f159526338b5bbb9fcac86dfd2b (diff)
parentb3431b1d9ee5121883d307cff0b62b7e53369891 (diff)
downloadcompcert-kvx-168393089024b5f926836cb813fddf14e6b6e4d4.tar.gz
compcert-kvx-168393089024b5f926836cb813fddf14e6b6e4d4.zip
Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div
(unfinished)
Diffstat (limited to 'test/monniaux/cse2')
-rw-r--r--test/monniaux/cse2/loopaccess.c7
-rw-r--r--test/monniaux/cse2/loopinvariant.c7
-rw-r--r--test/monniaux/cse2/loopload.c5
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];
+}