aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/moves
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-01-08 13:02:37 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-01-08 13:02:37 +0100
commit65cdeb76c33ddb059632c9b227e5ab13c65c6b72 (patch)
tree4d24695bd0c270a06add6797ac3f3a3d3ede29ef /test/monniaux/moves
parent2347476653201f154ffaea84f520e41cc0f32090 (diff)
downloadcompcert-kvx-65cdeb76c33ddb059632c9b227e5ab13c65c6b72.tar.gz
compcert-kvx-65cdeb76c33ddb059632c9b227e5ab13c65c6b72.zip
add an example
Diffstat (limited to 'test/monniaux/moves')
-rw-r--r--test/monniaux/moves/array.c18
1 files changed, 18 insertions, 0 deletions
diff --git a/test/monniaux/moves/array.c b/test/monniaux/moves/array.c
new file mode 100644
index 00000000..faa1d96b
--- /dev/null
+++ b/test/monniaux/moves/array.c
@@ -0,0 +1,18 @@
+void incr_double_array(double *t) {
+ double x0 = 1.0;
+ double t0 = t[0];
+ double x1 = 1.0;
+ double t1 = t[1];
+ double x2 = 1.0;
+ double t2 = t[2];
+ double x3 = 1.0;
+ double t3 = t[3];
+ t0 = t0 + x0;
+ t1 = t1 + x1;
+ t2 = t2 + x2;
+ t3 = t3 + x3;
+ t[0] = t0;
+ t[1] = t1;
+ t[2] = t2;
+ t[3] = t3;
+}