diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-03 17:17:33 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-03 17:17:33 +0100 |
| commit | 9ac665bba44e45eed8517d8f40a1b41c51051348 (patch) | |
| tree | af82f36389926343b91eb94777853c8e4ea17f80 /test/monniaux/cse2/loopinvariant.c | |
| parent | b71f1c635f20550f6ffdea7f99e65b8516d46768 (diff) | |
| parent | 1dd98d18c57abdbc8dc50bbef729e8a898d55aad (diff) | |
| download | compcert-kvx-9ac665bba44e45eed8517d8f40a1b41c51051348.tar.gz compcert-kvx-9ac665bba44e45eed8517d8f40a1b41c51051348.zip | |
Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2
Diffstat (limited to 'test/monniaux/cse2/loopinvariant.c')
| -rw-r--r-- | test/monniaux/cse2/loopinvariant.c | 7 |
1 files changed, 7 insertions, 0 deletions
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; +} |