aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/cse2
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-19 19:50:14 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-19 19:50:14 +0200
commitd0163625ad55f8b01a3c002dd52be83b8a26e35e (patch)
treed8aa19e8cf7f69775ff5233897c7939e344010e5 /test/monniaux/cse2
parent9010b8750aecd3a1ab45944b7dd4af3f33768f71 (diff)
downloadcompcert-kvx-d0163625ad55f8b01a3c002dd52be83b8a26e35e.tar.gz
compcert-kvx-d0163625ad55f8b01a3c002dd52be83b8a26e35e.zip
test whether the instructions are allowed
Diffstat (limited to 'test/monniaux/cse2')
-rw-r--r--test/monniaux/cse2/noloopinvariant.c6
1 files changed, 6 insertions, 0 deletions
diff --git a/test/monniaux/cse2/noloopinvariant.c b/test/monniaux/cse2/noloopinvariant.c
new file mode 100644
index 00000000..5c7789bf
--- /dev/null
+++ b/test/monniaux/cse2/noloopinvariant.c
@@ -0,0 +1,6 @@
+int toto(int *t, int n) {
+ for(int i=1; i<n; i++) {
+ if (t[i] > t[0]) return i;
+ }
+ return 0;
+}