aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-09 11:39:50 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-09 11:39:50 +0100
commitf01d490fad2fbf7fb7a2e0861075ca6c09976ec4 (patch)
tree66dc608ffc18bb34ae1fdd28ac3d97feae4f1f38
parent79c039d7b33878d00f22ad8542dc30a78aa8b70a (diff)
downloadcompcert-kvx-f01d490fad2fbf7fb7a2e0861075ca6c09976ec4.tar.gz
compcert-kvx-f01d490fad2fbf7fb7a2e0861075ca6c09976ec4.zip
redundant tests
-rw-r--r--test/monniaux/if/if2.c11
1 files changed, 11 insertions, 0 deletions
diff --git a/test/monniaux/if/if2.c b/test/monniaux/if/if2.c
new file mode 100644
index 00000000..2a6d5507
--- /dev/null
+++ b/test/monniaux/if/if2.c
@@ -0,0 +1,11 @@
+int toto(int x) {
+ if (2*x+1 >= 3) {
+ if (2*x+1 >= 3) {
+ return 3;
+ } else {
+ return 2;
+ }
+ } else {
+ return 1;
+ }
+}