From 0605b34e3531b5cc9df7c541c96aab25f87b7658 Mon Sep 17 00:00:00 2001
From: Dario Pinto <dario.pinto@cea.fr>
Date: Mon, 31 Aug 2020 10:55:03 +0200
Subject: [PATCH] add reducercommutativity
---
svcomp/normalize.sh | 5 +
.../reducercommutativity/.frama-c/GNUmakefile | 69 +++++
.../.frama-c/eval_summary.txt | 242 ++++++++++++++++++
.../.frama-c/evaluate_case.sh | 129 ++++++++++
svcomp/reducercommutativity/.frama-c/path.mk | 1 +
svcomp/reducercommutativity/LICENSE.txt | 23 ++
svcomp/reducercommutativity/Makefile | 3 +
svcomp/reducercommutativity/README.txt | 12 +
svcomp/reducercommutativity/avg.c | 58 +++++
svcomp/reducercommutativity/avg.yml | 13 +
svcomp/reducercommutativity/avg05-1.c | 59 +++++
svcomp/reducercommutativity/avg05-1.yml | 13 +
svcomp/reducercommutativity/avg05-2.c | 54 ++++
svcomp/reducercommutativity/avg05-2.yml | 8 +
svcomp/reducercommutativity/avg10-1.c | 54 ++++
svcomp/reducercommutativity/avg10-1.yml | 8 +
svcomp/reducercommutativity/avg10-2.c | 59 +++++
svcomp/reducercommutativity/avg10-2.yml | 13 +
svcomp/reducercommutativity/avg20-1.c | 54 ++++
svcomp/reducercommutativity/avg20-1.yml | 8 +
svcomp/reducercommutativity/avg20-2.c | 59 +++++
svcomp/reducercommutativity/avg20-2.yml | 11 +
svcomp/reducercommutativity/avg40-1.c | 54 ++++
svcomp/reducercommutativity/avg40-1.yml | 8 +
svcomp/reducercommutativity/avg40-2.c | 59 +++++
svcomp/reducercommutativity/avg40-2.yml | 11 +
svcomp/reducercommutativity/avg60-1.c | 59 +++++
svcomp/reducercommutativity/avg60-1.yml | 11 +
svcomp/reducercommutativity/avg60-2.c | 54 ++++
svcomp/reducercommutativity/avg60-2.yml | 8 +
.../reducercommutativity/frama-c-cgc-path.mk | 8 +
svcomp/reducercommutativity/max.c | 59 +++++
svcomp/reducercommutativity/max.yml | 13 +
svcomp/reducercommutativity/max05-1.c | 59 +++++
svcomp/reducercommutativity/max05-1.yml | 13 +
svcomp/reducercommutativity/max05-2.c | 54 ++++
svcomp/reducercommutativity/max05-2.yml | 8 +
svcomp/reducercommutativity/max10-1.c | 59 +++++
svcomp/reducercommutativity/max10-1.yml | 13 +
svcomp/reducercommutativity/max10-2.c | 54 ++++
svcomp/reducercommutativity/max10-2.yml | 8 +
svcomp/reducercommutativity/max20-1.c | 59 +++++
svcomp/reducercommutativity/max20-1.yml | 11 +
svcomp/reducercommutativity/max20-2.c | 54 ++++
svcomp/reducercommutativity/max20-2.yml | 8 +
svcomp/reducercommutativity/max40-1.c | 59 +++++
svcomp/reducercommutativity/max40-1.yml | 11 +
svcomp/reducercommutativity/max40-2.c | 54 ++++
svcomp/reducercommutativity/max40-2.yml | 8 +
svcomp/reducercommutativity/max60-1.c | 54 ++++
svcomp/reducercommutativity/max60-1.yml | 8 +
svcomp/reducercommutativity/max60-2.c | 59 +++++
svcomp/reducercommutativity/max60-2.yml | 11 +
svcomp/reducercommutativity/rangesum.c | 74 ++++++
svcomp/reducercommutativity/rangesum.yml | 14 +
svcomp/reducercommutativity/rangesum05.c | 70 +++++
svcomp/reducercommutativity/rangesum05.yml | 14 +
svcomp/reducercommutativity/rangesum10.c | 70 +++++
svcomp/reducercommutativity/rangesum10.yml | 14 +
svcomp/reducercommutativity/rangesum20.c | 70 +++++
svcomp/reducercommutativity/rangesum20.yml | 12 +
svcomp/reducercommutativity/rangesum40.c | 70 +++++
svcomp/reducercommutativity/rangesum40.yml | 12 +
svcomp/reducercommutativity/rangesum60.c | 70 +++++
svcomp/reducercommutativity/rangesum60.yml | 12 +
svcomp/reducercommutativity/sep.c | 62 +++++
svcomp/reducercommutativity/sep.yml | 13 +
svcomp/reducercommutativity/sep05-1.c | 62 +++++
svcomp/reducercommutativity/sep05-1.yml | 13 +
svcomp/reducercommutativity/sep05-2.c | 57 +++++
svcomp/reducercommutativity/sep05-2.yml | 8 +
svcomp/reducercommutativity/sep10-1.c | 57 +++++
svcomp/reducercommutativity/sep10-1.yml | 8 +
svcomp/reducercommutativity/sep10-2.c | 62 +++++
svcomp/reducercommutativity/sep10-2.yml | 11 +
svcomp/reducercommutativity/sep20-1.c | 62 +++++
svcomp/reducercommutativity/sep20-1.yml | 11 +
svcomp/reducercommutativity/sep20-2.c | 57 +++++
svcomp/reducercommutativity/sep20-2.yml | 8 +
svcomp/reducercommutativity/sep40-1.c | 62 +++++
svcomp/reducercommutativity/sep40-1.yml | 11 +
svcomp/reducercommutativity/sep40-2.c | 57 +++++
svcomp/reducercommutativity/sep40-2.yml | 8 +
svcomp/reducercommutativity/sep60-1.c | 57 +++++
svcomp/reducercommutativity/sep60-1.yml | 8 +
svcomp/reducercommutativity/sep60-2.c | 62 +++++
svcomp/reducercommutativity/sep60-2.yml | 11 +
svcomp/reducercommutativity/sum.c | 59 +++++
svcomp/reducercommutativity/sum.yml | 13 +
svcomp/reducercommutativity/sum05-1.c | 54 ++++
svcomp/reducercommutativity/sum05-1.yml | 8 +
svcomp/reducercommutativity/sum05-2.c | 59 +++++
svcomp/reducercommutativity/sum05-2.yml | 13 +
svcomp/reducercommutativity/sum10-1.c | 59 +++++
svcomp/reducercommutativity/sum10-1.yml | 13 +
svcomp/reducercommutativity/sum10-2.c | 54 ++++
svcomp/reducercommutativity/sum10-2.yml | 8 +
svcomp/reducercommutativity/sum20-1.c | 54 ++++
svcomp/reducercommutativity/sum20-1.yml | 8 +
svcomp/reducercommutativity/sum20-2.c | 59 +++++
svcomp/reducercommutativity/sum20-2.yml | 11 +
svcomp/reducercommutativity/sum40-1.c | 54 ++++
svcomp/reducercommutativity/sum40-1.yml | 8 +
svcomp/reducercommutativity/sum40-2.c | 59 +++++
svcomp/reducercommutativity/sum40-2.yml | 11 +
svcomp/reducercommutativity/sum60-1.c | 54 ++++
svcomp/reducercommutativity/sum60-1.yml | 8 +
svcomp/reducercommutativity/sum60-2.c | 59 +++++
svcomp/reducercommutativity/sum60-2.yml | 11 +
109 files changed, 3968 insertions(+)
create mode 100644 svcomp/reducercommutativity/.frama-c/GNUmakefile
create mode 100644 svcomp/reducercommutativity/.frama-c/eval_summary.txt
create mode 100755 svcomp/reducercommutativity/.frama-c/evaluate_case.sh
create mode 120000 svcomp/reducercommutativity/.frama-c/path.mk
create mode 100644 svcomp/reducercommutativity/LICENSE.txt
create mode 100644 svcomp/reducercommutativity/Makefile
create mode 100644 svcomp/reducercommutativity/README.txt
create mode 100644 svcomp/reducercommutativity/avg.c
create mode 100644 svcomp/reducercommutativity/avg.yml
create mode 100644 svcomp/reducercommutativity/avg05-1.c
create mode 100644 svcomp/reducercommutativity/avg05-1.yml
create mode 100644 svcomp/reducercommutativity/avg05-2.c
create mode 100644 svcomp/reducercommutativity/avg05-2.yml
create mode 100644 svcomp/reducercommutativity/avg10-1.c
create mode 100644 svcomp/reducercommutativity/avg10-1.yml
create mode 100644 svcomp/reducercommutativity/avg10-2.c
create mode 100644 svcomp/reducercommutativity/avg10-2.yml
create mode 100644 svcomp/reducercommutativity/avg20-1.c
create mode 100644 svcomp/reducercommutativity/avg20-1.yml
create mode 100644 svcomp/reducercommutativity/avg20-2.c
create mode 100644 svcomp/reducercommutativity/avg20-2.yml
create mode 100644 svcomp/reducercommutativity/avg40-1.c
create mode 100644 svcomp/reducercommutativity/avg40-1.yml
create mode 100644 svcomp/reducercommutativity/avg40-2.c
create mode 100644 svcomp/reducercommutativity/avg40-2.yml
create mode 100644 svcomp/reducercommutativity/avg60-1.c
create mode 100644 svcomp/reducercommutativity/avg60-1.yml
create mode 100644 svcomp/reducercommutativity/avg60-2.c
create mode 100644 svcomp/reducercommutativity/avg60-2.yml
create mode 100644 svcomp/reducercommutativity/frama-c-cgc-path.mk
create mode 100644 svcomp/reducercommutativity/max.c
create mode 100644 svcomp/reducercommutativity/max.yml
create mode 100644 svcomp/reducercommutativity/max05-1.c
create mode 100644 svcomp/reducercommutativity/max05-1.yml
create mode 100644 svcomp/reducercommutativity/max05-2.c
create mode 100644 svcomp/reducercommutativity/max05-2.yml
create mode 100644 svcomp/reducercommutativity/max10-1.c
create mode 100644 svcomp/reducercommutativity/max10-1.yml
create mode 100644 svcomp/reducercommutativity/max10-2.c
create mode 100644 svcomp/reducercommutativity/max10-2.yml
create mode 100644 svcomp/reducercommutativity/max20-1.c
create mode 100644 svcomp/reducercommutativity/max20-1.yml
create mode 100644 svcomp/reducercommutativity/max20-2.c
create mode 100644 svcomp/reducercommutativity/max20-2.yml
create mode 100644 svcomp/reducercommutativity/max40-1.c
create mode 100644 svcomp/reducercommutativity/max40-1.yml
create mode 100644 svcomp/reducercommutativity/max40-2.c
create mode 100644 svcomp/reducercommutativity/max40-2.yml
create mode 100644 svcomp/reducercommutativity/max60-1.c
create mode 100644 svcomp/reducercommutativity/max60-1.yml
create mode 100644 svcomp/reducercommutativity/max60-2.c
create mode 100644 svcomp/reducercommutativity/max60-2.yml
create mode 100644 svcomp/reducercommutativity/rangesum.c
create mode 100644 svcomp/reducercommutativity/rangesum.yml
create mode 100644 svcomp/reducercommutativity/rangesum05.c
create mode 100644 svcomp/reducercommutativity/rangesum05.yml
create mode 100644 svcomp/reducercommutativity/rangesum10.c
create mode 100644 svcomp/reducercommutativity/rangesum10.yml
create mode 100644 svcomp/reducercommutativity/rangesum20.c
create mode 100644 svcomp/reducercommutativity/rangesum20.yml
create mode 100644 svcomp/reducercommutativity/rangesum40.c
create mode 100644 svcomp/reducercommutativity/rangesum40.yml
create mode 100644 svcomp/reducercommutativity/rangesum60.c
create mode 100644 svcomp/reducercommutativity/rangesum60.yml
create mode 100644 svcomp/reducercommutativity/sep.c
create mode 100644 svcomp/reducercommutativity/sep.yml
create mode 100644 svcomp/reducercommutativity/sep05-1.c
create mode 100644 svcomp/reducercommutativity/sep05-1.yml
create mode 100644 svcomp/reducercommutativity/sep05-2.c
create mode 100644 svcomp/reducercommutativity/sep05-2.yml
create mode 100644 svcomp/reducercommutativity/sep10-1.c
create mode 100644 svcomp/reducercommutativity/sep10-1.yml
create mode 100644 svcomp/reducercommutativity/sep10-2.c
create mode 100644 svcomp/reducercommutativity/sep10-2.yml
create mode 100644 svcomp/reducercommutativity/sep20-1.c
create mode 100644 svcomp/reducercommutativity/sep20-1.yml
create mode 100644 svcomp/reducercommutativity/sep20-2.c
create mode 100644 svcomp/reducercommutativity/sep20-2.yml
create mode 100644 svcomp/reducercommutativity/sep40-1.c
create mode 100644 svcomp/reducercommutativity/sep40-1.yml
create mode 100644 svcomp/reducercommutativity/sep40-2.c
create mode 100644 svcomp/reducercommutativity/sep40-2.yml
create mode 100644 svcomp/reducercommutativity/sep60-1.c
create mode 100644 svcomp/reducercommutativity/sep60-1.yml
create mode 100644 svcomp/reducercommutativity/sep60-2.c
create mode 100644 svcomp/reducercommutativity/sep60-2.yml
create mode 100644 svcomp/reducercommutativity/sum.c
create mode 100644 svcomp/reducercommutativity/sum.yml
create mode 100644 svcomp/reducercommutativity/sum05-1.c
create mode 100644 svcomp/reducercommutativity/sum05-1.yml
create mode 100644 svcomp/reducercommutativity/sum05-2.c
create mode 100644 svcomp/reducercommutativity/sum05-2.yml
create mode 100644 svcomp/reducercommutativity/sum10-1.c
create mode 100644 svcomp/reducercommutativity/sum10-1.yml
create mode 100644 svcomp/reducercommutativity/sum10-2.c
create mode 100644 svcomp/reducercommutativity/sum10-2.yml
create mode 100644 svcomp/reducercommutativity/sum20-1.c
create mode 100644 svcomp/reducercommutativity/sum20-1.yml
create mode 100644 svcomp/reducercommutativity/sum20-2.c
create mode 100644 svcomp/reducercommutativity/sum20-2.yml
create mode 100644 svcomp/reducercommutativity/sum40-1.c
create mode 100644 svcomp/reducercommutativity/sum40-1.yml
create mode 100644 svcomp/reducercommutativity/sum40-2.c
create mode 100644 svcomp/reducercommutativity/sum40-2.yml
create mode 100644 svcomp/reducercommutativity/sum60-1.c
create mode 100644 svcomp/reducercommutativity/sum60-1.yml
create mode 100644 svcomp/reducercommutativity/sum60-2.c
create mode 100644 svcomp/reducercommutativity/sum60-2.yml
diff --git a/svcomp/normalize.sh b/svcomp/normalize.sh
index 2e3fc89fa..a88e78488 100755
--- a/svcomp/normalize.sh
+++ b/svcomp/normalize.sh
@@ -11,3 +11,8 @@ sed -i 's/__VERIFIER_nondet_uchar()/Frama_C_interval(0, UCHAR_MAX)/g' $*
sed -i 's/__VERIFIER_nondet_char()/Frama_C_interval(CHAR_MIN, CHAR_MAX)/g' $*
sed -i 's/__VERIFIER_nondet_ulong()/Frama_C_unsigned_long_interval(0, ULONG_MAX)/g' $*
+sed -i 's/extern int Frama_C_interval(INT_MIN, INT_MAX);//g' $*
+sed -i 's/extern short Frama_C_interval(SHRT_MIN, SHRT_MAX);//g' $*
+sed -i 's/extern unsigned chard Frama_C_interval(0, UCHAR_MAX);//g' $*
+sed -i 's/extern char Frama_C_interval(CHAR_MIN, CHAR_MAX);//g' $*
+sed -i 's/exterm unsigned long Frama_C_unsigned_long_interval(0, ULONG_MAX);//g' $*
diff --git a/svcomp/reducercommutativity/.frama-c/GNUmakefile b/svcomp/reducercommutativity/.frama-c/GNUmakefile
new file mode 100644
index 000000000..9bbcdbac5
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/GNUmakefile
@@ -0,0 +1,69 @@
+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk
+FRAMAC ?= frama-c
+include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+###############################################################################
+
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+
+MACHDEP = x86_32
+
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS += \
+ -D__FC_PATCHED \
+ -I../../lib \
+ -I../../../frama-c/share/libc
+
+## General flags
+FCFLAGS += \
+ -add-symbolic-path=.:..\
+ -kernel-warn-key annot:missing-spec=abort \
+ -kernel-warn-key typing:implicit-function-declaration=abort \
+ -absolute-valid-range 0x4347C000-0x4347FFFF \
+ -c11\
+
+## Eva-specific flags
+EVAFLAGS += \
+ -eva-precision 5 \
+ -eva-warn-key builtins:missing-spec=abort \
+
+## GUI-only flags
+FCGUIFLAGS += \
+ -add-symbolic-path=.:..\
+
+# exclude files with recursive functions, and those testing memory leaks
+filter-out-substring = $(foreach v,$(2),$(if $(findstring $(1),$(v)),,$(v)))
+SRCS:=$(sort $(wildcard ../*.c))
+
+# [target] converts a file name into a suitable target name,
+# removing the initial '../', the final '.c'.
+target = $(subst /,/,$(patsubst %.c,%,$(1:../%=%)))
+
+EVA_TARGETS:=$(foreach s,$(SRCS),$(call target,$(s)).eva)
+TARGETS:=$(EVA_TARGETS)
+
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+define generate-parse-rules =
+$(call target,$(1)).parse: $(if $(findstring cross_file,$(1)),,) $(1)
+$(call target,$(1)).parse: SRCS += ../../../frama-c/share/libc/__fc_builtin.c
+
+$(call target,$(1)).eva/eval.txt: $(call target, $(1)).eva
+ ./evaluate_case.sh $(subst .c,,$(1)).yml $$</alarms.csv $$</nonterm.log > $$</eval.txt
+endef
+$(foreach s,$(SRCS),$(eval $(call generate-parse-rules,$(s))))
+
+eval_summary.txt: $(addsuffix /eval.txt, $(TARGETS))
+ cat $^ > eval_summary.txt
+
+evaluate: eval_summary.txt
+.PHONY: eval_summary.txt
+
+fclean: clean
+ rm eval_summary.txt
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+###############################################################################
diff --git a/svcomp/reducercommutativity/.frama-c/eval_summary.txt b/svcomp/reducercommutativity/.frama-c/eval_summary.txt
new file mode 100644
index 000000000..97b24a7ca
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/eval_summary.txt
@@ -0,0 +1,242 @@
+
+Termination spec: true
+avg.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+avg.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Termination spec: true
+avg05-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+avg05-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg05-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg10-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+avg10-2.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+avg10-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg20-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+avg20-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg40-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+avg40-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Unreachability spec: true
+avg60-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg60-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+max.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+max.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Termination spec: true
+max05-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+max05-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max05-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+max10-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+max10-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max10-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+max20-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max20-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+max40-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max40-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+max60-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+max60-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Termination spec: true
+rangesum.eva/alarms.csv (true): Valid
+
+Unreachability spec: false
+rangesum.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Termination spec: true
+rangesum05.eva/alarms.csv (true): Valid
+
+Unreachability spec: false
+rangesum05.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Termination spec: true
+rangesum10.eva/alarms.csv (true): Valid
+
+Unreachability spec: false
+rangesum10.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Unreachability spec: false
+rangesum20.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Unreachability spec: false
+rangesum40.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Unreachability spec: false
+rangesum60.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Termination spec: true
+sep.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sep.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Termination spec: true
+sep05-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sep05-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep05-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep10-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sep10-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Unreachability spec: true
+sep20-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep20-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sep40-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep40-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep60-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sep60-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Termination spec: true
+sum.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sum.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Defined Behavior spec: false
+sum05-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+sum05-2.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sum05-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Termination spec: true
+sum10-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sum10-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum10-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum20-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sum20-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum40-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sum40-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum60-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sum60-2.eva/alarms.csv (true): Valid
+__________________________________
diff --git a/svcomp/reducercommutativity/.frama-c/evaluate_case.sh b/svcomp/reducercommutativity/.frama-c/evaluate_case.sh
new file mode 100755
index 000000000..f6e23d8d0
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/evaluate_case.sh
@@ -0,0 +1,129 @@
+#!/bin/bash -u
+
+# Script is not yet complete and shouldn't yet be used
+# https://sv-comp.sosy-lab.org/2020/rules.php
+# to check the meaning of all specs in *.yml files
+
+if [ $# -lt 2 ]; then
+ echo "usage: $0 (dotyml_file_spec) path/to/alarms.csv path/to/nonterm.log"
+ exit 1
+fi
+
+#set argument variables
+dotyml="$1"
+alarmcsv="$2"
+nontermlog="$3"
+
+#get number of lines in FramaC's target alarm.csv file
+alarms=$(wc -l $alarmcsv | cut -d' ' -f1)
+
+#check and get FramaC's conclusion
+valid_deref=$(grep "index_bound" $alarmcsv)
+if [ -z "$valid_deref" ]; then
+ valid_deref=$(grep "mem_access" $alarmcsv)
+fi
+
+#check number of lines in target's nonterm.log
+nonterm=$(wc -l $nontermlog | cut -d' ' -f1)
+
+#check and get spec true/false
+termination=$(grep "property_file: ../properties/termination.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+#check and get spec true/false
+memsafety=$(grep "property_file: ../properties/valid-memsafety.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+#check and get spec true/false
+defbehavior=$(grep "property_file: ../properties/def-behavior.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+#check and get spec true/false
+unreachability=$(grep "property_file: ../properties/unreach-call.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+## This part is suppose to establish if program must terminate.
+# if $termination = true then it must terminate one way or another, call to abort is accepted
+# else if $termination = false, then program is most likely an infinite loop and must not exit by ordinary means, ie should be interrupted
+#
+# NO FALSE CASE IN ARRAY-EXAMPLES
+if [ -n "$termination" ]; then
+ printf "\nTermination spec: $termination\n"
+ case $termination in
+ "true")
+ if [ "$nonterm" -ge 0 ]; then
+ echo "$2 ($termination): Valid"
+ else
+ echo "$2 ($termination): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in termination :C.\n"
+ exit 1
+ esac
+fi
+
+## This part is suppose to establish whether the error function __VERIFIER_error() was reached during a finite execution of the program.
+#
+# if $unreachability = true, then given function must never be reached in any path of the execution.
+# else if $unreachability = false, then given __VERIFIER_error() function must be reached at some point of the program, and program must exit by a call to the abort(); function.
+#
+#
+if [ -n "$unreachability" ]; then
+ printf "\nUnreachability spec: $unreachability\n"
+ case $unreachability in
+ "true")
+ if [ "$nonterm" -eq 0 ]; then
+ echo "$2 ($unreachability): Valid"
+ else
+ echo "$2 ($unreachability): Imprecise"
+ fi
+ ;;
+ "false")
+ if [ "$nonterm" -ne 0 ]; then
+ echo "$2 ($unreachability): Valid"
+ else
+ echo "$2 ($unreachability): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in unreachability :C.\n"
+ exit 1
+ esac
+fi
+
+## This part tends to adress the memsafety spec. To verify a set of subspec found in all targets.yml files
+#
+# The only memsafety subspec present in ARRAY-EXAMPLES is VALID-DEREF. Therefore it's the only one this script checks
+#
+#FALSE case is omitted because of its absence in ARRAY-EXAMPLES
+if [ -n "$memsafety" ]; then
+ printf "\nValid-Memsafety spec: $memsafety\n"
+ case $memsafety in
+ "false")
+ if [ -n "$valid_deref" ]; then
+ echo "$2 ($memsafety): Valid"
+ else
+ echo "$2 ($memsafety): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in memsafety :C.\n"
+ exit 1
+ esac
+fi
+
+## This part tends to handle the one and only case of Def-behaviour spec.
+# it is FALSE and is found in standard_find_ground-2.yml and standard_sentinel-1.yml
+if [ -n "$defbehavior" ]; then
+ printf "\nDefined Behavior spec: $defbehavior\n"
+ case $defbehavior in
+ "false")
+ if [ "$alarms" -ne 0 ]; then
+ echo "$2 ($defbehavior): Valid"
+ else
+ echo "$2 ($defbehavior): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in defbehavior :C.\n"
+ exit 1
+ esac
+fi
+echo "__________________________________"
diff --git a/svcomp/reducercommutativity/.frama-c/path.mk b/svcomp/reducercommutativity/.frama-c/path.mk
new file mode 120000
index 000000000..261a4f4b4
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/path.mk
@@ -0,0 +1 @@
+../frama-c-cgc-path.mk
\ No newline at end of file
diff --git a/svcomp/reducercommutativity/LICENSE.txt b/svcomp/reducercommutativity/LICENSE.txt
new file mode 100644
index 000000000..ebbd4f95c
--- /dev/null
+++ b/svcomp/reducercommutativity/LICENSE.txt
@@ -0,0 +1,23 @@
+Copyright (c) 2015, Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright notice,
+ this list of conditions and the following disclaimer.
+ * Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.
\ No newline at end of file
diff --git a/svcomp/reducercommutativity/Makefile b/svcomp/reducercommutativity/Makefile
new file mode 100644
index 000000000..49b2905c1
--- /dev/null
+++ b/svcomp/reducercommutativity/Makefile
@@ -0,0 +1,3 @@
+LEVEL := ../
+
+include $(LEVEL)/Makefile.config
diff --git a/svcomp/reducercommutativity/README.txt b/svcomp/reducercommutativity/README.txt
new file mode 100644
index 000000000..0093aafbf
--- /dev/null
+++ b/svcomp/reducercommutativity/README.txt
@@ -0,0 +1,12 @@
+Benchmarks used in the paper "Commutativity of Reducers"
+which was published at TACAS 2015 and
+written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+
+We checks if a function is "deterministic" w.r.t. all possible permutations
+of an input array. Such property is desirable for reducers in the
+map-reduce programming model. It ensures that the program always computes
+the same results on the same input data set.
+
+Submitted by Matthias Heizmann.
+
diff --git a/svcomp/reducercommutativity/avg.c b/svcomp/reducercommutativity/avg.c
new file mode 100644
index 000000000..4633c5503
--- /dev/null
+++ b/svcomp/reducercommutativity/avg.c
@@ -0,0 +1,58 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun avg
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg.yml b/svcomp/reducercommutativity/avg.yml
new file mode 100644
index 000000000..8ca5b57ab
--- /dev/null
+++ b/svcomp/reducercommutativity/avg.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: avg_true-unreach-call_true-termination.i
+input_files: 'avg.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg05-1.c b/svcomp/reducercommutativity/avg05-1.c
new file mode 100644
index 000000000..f0d890c51
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg05-1.yml b/svcomp/reducercommutativity/avg05-1.yml
new file mode 100644
index 000000000..6662db49c
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: avg05_true-unreach-call_true-termination.i
+input_files: 'avg05-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg05-2.c b/svcomp/reducercommutativity/avg05-2.c
new file mode 100644
index 000000000..b575df004
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg05-2.yml b/svcomp/reducercommutativity/avg05-2.yml
new file mode 100644
index 000000000..916247cbb
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg05_false-def-behavior.i
+input_files: 'avg05-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg10-1.c b/svcomp/reducercommutativity/avg10-1.c
new file mode 100644
index 000000000..9caa88d88
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg10-1.yml b/svcomp/reducercommutativity/avg10-1.yml
new file mode 100644
index 000000000..0e3fd1467
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg10_false-def-behavior.i
+input_files: 'avg10-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg10-2.c b/svcomp/reducercommutativity/avg10-2.c
new file mode 100644
index 000000000..63229ae34
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg10-2.yml b/svcomp/reducercommutativity/avg10-2.yml
new file mode 100644
index 000000000..61e0cbb6c
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-2.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: avg10_true-unreach-call_true-termination.i
+input_files: 'avg10-2.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg20-1.c b/svcomp/reducercommutativity/avg20-1.c
new file mode 100644
index 000000000..a47d3434e
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg20-1.yml b/svcomp/reducercommutativity/avg20-1.yml
new file mode 100644
index 000000000..ca77fdc56
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg20_false-def-behavior.i
+input_files: 'avg20-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg20-2.c b/svcomp/reducercommutativity/avg20-2.c
new file mode 100644
index 000000000..7eaf13c03
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg20-2.yml b/svcomp/reducercommutativity/avg20-2.yml
new file mode 100644
index 000000000..89db14bbc
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: avg20_true-unreach-call.i
+input_files: 'avg20-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg40-1.c b/svcomp/reducercommutativity/avg40-1.c
new file mode 100644
index 000000000..1125af7f2
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg40-1.yml b/svcomp/reducercommutativity/avg40-1.yml
new file mode 100644
index 000000000..32cb868c8
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg40_false-def-behavior.i
+input_files: 'avg40-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg40-2.c b/svcomp/reducercommutativity/avg40-2.c
new file mode 100644
index 000000000..c3169c537
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg40-2.yml b/svcomp/reducercommutativity/avg40-2.yml
new file mode 100644
index 000000000..8687001ea
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: avg40_true-unreach-call.i
+input_files: 'avg40-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg60-1.c b/svcomp/reducercommutativity/avg60-1.c
new file mode 100644
index 000000000..48aa6b858
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg60-1.yml b/svcomp/reducercommutativity/avg60-1.yml
new file mode 100644
index 000000000..a80991cc7
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: avg60_true-unreach-call.i
+input_files: 'avg60-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg60-2.c b/svcomp/reducercommutativity/avg60-2.c
new file mode 100644
index 000000000..8f566d3e2
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg60-2.yml b/svcomp/reducercommutativity/avg60-2.yml
new file mode 100644
index 000000000..891f7539c
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg60_false-def-behavior.i
+input_files: 'avg60-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/frama-c-cgc-path.mk b/svcomp/reducercommutativity/frama-c-cgc-path.mk
new file mode 100644
index 000000000..f6e877ad3
--- /dev/null
+++ b/svcomp/reducercommutativity/frama-c-cgc-path.mk
@@ -0,0 +1,8 @@
+FRAMAC_DIR=../../../frama-c/build/bin
+ifeq ($(wildcard $(FRAMAC_DIR)),)
+# Frama-C not installed locally; using the version in the PATH
+else
+FRAMAC=$(FRAMAC_DIR)/frama-c
+FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui
+FRAMAC_CONFIG=$(FRAMAC_DIR)/frama-c-config
+endif
diff --git a/svcomp/reducercommutativity/max.c b/svcomp/reducercommutativity/max.c
new file mode 100644
index 000000000..21e1400c8
--- /dev/null
+++ b/svcomp/reducercommutativity/max.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max.yml b/svcomp/reducercommutativity/max.yml
new file mode 100644
index 000000000..4b4bfd108
--- /dev/null
+++ b/svcomp/reducercommutativity/max.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: max_true-unreach-call_true-termination.i
+input_files: 'max.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max05-1.c b/svcomp/reducercommutativity/max05-1.c
new file mode 100644
index 000000000..ba4b6ad0b
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max05-1.yml b/svcomp/reducercommutativity/max05-1.yml
new file mode 100644
index 000000000..c2335acf3
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: max05_true-unreach-call_true-termination.i
+input_files: 'max05-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max05-2.c b/svcomp/reducercommutativity/max05-2.c
new file mode 100644
index 000000000..31f4b9dbb
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max05-2.yml b/svcomp/reducercommutativity/max05-2.yml
new file mode 100644
index 000000000..c0614d6ae
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max05_false-def-behavior.i
+input_files: 'max05-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max10-1.c b/svcomp/reducercommutativity/max10-1.c
new file mode 100644
index 000000000..2a6d751c0
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max10-1.yml b/svcomp/reducercommutativity/max10-1.yml
new file mode 100644
index 000000000..8a7cd3f1c
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: max10_true-unreach-call_true-termination.i
+input_files: 'max10-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max10-2.c b/svcomp/reducercommutativity/max10-2.c
new file mode 100644
index 000000000..e37284a12
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max10-2.yml b/svcomp/reducercommutativity/max10-2.yml
new file mode 100644
index 000000000..702485612
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max10_false-def-behavior.i
+input_files: 'max10-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max20-1.c b/svcomp/reducercommutativity/max20-1.c
new file mode 100644
index 000000000..4cb0ef709
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max20-1.yml b/svcomp/reducercommutativity/max20-1.yml
new file mode 100644
index 000000000..439cc7ae6
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: max20_true-unreach-call.i
+input_files: 'max20-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max20-2.c b/svcomp/reducercommutativity/max20-2.c
new file mode 100644
index 000000000..ab4a9199e
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max20-2.yml b/svcomp/reducercommutativity/max20-2.yml
new file mode 100644
index 000000000..a20610d97
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max20_false-def-behavior.i
+input_files: 'max20-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max40-1.c b/svcomp/reducercommutativity/max40-1.c
new file mode 100644
index 000000000..631e18b11
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max40-1.yml b/svcomp/reducercommutativity/max40-1.yml
new file mode 100644
index 000000000..f6cc70bd1
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: max40_true-unreach-call.i
+input_files: 'max40-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max40-2.c b/svcomp/reducercommutativity/max40-2.c
new file mode 100644
index 000000000..a7c688698
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max40-2.yml b/svcomp/reducercommutativity/max40-2.yml
new file mode 100644
index 000000000..f7f67210f
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max40_false-def-behavior.i
+input_files: 'max40-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max60-1.c b/svcomp/reducercommutativity/max60-1.c
new file mode 100644
index 000000000..4f80338b9
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max60-1.yml b/svcomp/reducercommutativity/max60-1.yml
new file mode 100644
index 000000000..096f1f776
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max60_false-def-behavior.i
+input_files: 'max60-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max60-2.c b/svcomp/reducercommutativity/max60-2.c
new file mode 100644
index 000000000..53bb33ca4
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max60-2.yml b/svcomp/reducercommutativity/max60-2.yml
new file mode 100644
index 000000000..d1a7b0d82
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: max60_true-unreach-call.i
+input_files: 'max60-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum.c b/svcomp/reducercommutativity/rangesum.c
new file mode 100644
index 000000000..7215e5209
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum.c
@@ -0,0 +1,74 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum.yml b/svcomp/reducercommutativity/rangesum.yml
new file mode 100644
index 000000000..92285eca8
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum.yml
@@ -0,0 +1,14 @@
+format_version: '1.0'
+
+# old file name: rangesum_false-unreach-call_true-termination.i
+input_files: 'rangesum.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum05.c b/svcomp/reducercommutativity/rangesum05.c
new file mode 100644
index 000000000..2a93ec2c9
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum05.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum05.yml b/svcomp/reducercommutativity/rangesum05.yml
new file mode 100644
index 000000000..cab42acc8
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum05.yml
@@ -0,0 +1,14 @@
+format_version: '1.0'
+
+# old file name: rangesum05_false-unreach-call_true-termination.i
+input_files: 'rangesum05.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum10.c b/svcomp/reducercommutativity/rangesum10.c
new file mode 100644
index 000000000..c30189bd8
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum10.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum10.yml b/svcomp/reducercommutativity/rangesum10.yml
new file mode 100644
index 000000000..eff52436d
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum10.yml
@@ -0,0 +1,14 @@
+format_version: '1.0'
+
+# old file name: rangesum10_false-unreach-call_true-termination.i
+input_files: 'rangesum10.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum20.c b/svcomp/reducercommutativity/rangesum20.c
new file mode 100644
index 000000000..db062633f
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum20.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum20.yml b/svcomp/reducercommutativity/rangesum20.yml
new file mode 100644
index 000000000..7abccd978
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum20.yml
@@ -0,0 +1,12 @@
+format_version: '1.0'
+
+# old file name: rangesum20_false-unreach-call.i
+input_files: 'rangesum20.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum40.c b/svcomp/reducercommutativity/rangesum40.c
new file mode 100644
index 000000000..3525a4ece
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum40.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum40.yml b/svcomp/reducercommutativity/rangesum40.yml
new file mode 100644
index 000000000..e675584cf
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum40.yml
@@ -0,0 +1,12 @@
+format_version: '1.0'
+
+# old file name: rangesum40_false-unreach-call.i
+input_files: 'rangesum40.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum60.c b/svcomp/reducercommutativity/rangesum60.c
new file mode 100644
index 000000000..97b9d4b86
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum60.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum60.yml b/svcomp/reducercommutativity/rangesum60.yml
new file mode 100644
index 000000000..040d9eda1
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum60.yml
@@ -0,0 +1,12 @@
+format_version: '1.0'
+
+# old file name: rangesum60_false-unreach-call.i
+input_files: 'rangesum60.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep.c b/svcomp/reducercommutativity/sep.c
new file mode 100644
index 000000000..f446127a3
--- /dev/null
+++ b/svcomp/reducercommutativity/sep.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep.yml b/svcomp/reducercommutativity/sep.yml
new file mode 100644
index 000000000..dcb748a75
--- /dev/null
+++ b/svcomp/reducercommutativity/sep.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sep_true-unreach-call_true-termination.i
+input_files: 'sep.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep05-1.c b/svcomp/reducercommutativity/sep05-1.c
new file mode 100644
index 000000000..d1ffcf4e4
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-1.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep05-1.yml b/svcomp/reducercommutativity/sep05-1.yml
new file mode 100644
index 000000000..2b4ad690a
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sep05_true-unreach-call_true-termination.i
+input_files: 'sep05-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep05-2.c b/svcomp/reducercommutativity/sep05-2.c
new file mode 100644
index 000000000..747308e07
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-2.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep05-2.yml b/svcomp/reducercommutativity/sep05-2.yml
new file mode 100644
index 000000000..af8f4428b
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep05_false-def-behavior.i
+input_files: 'sep05-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep10-1.c b/svcomp/reducercommutativity/sep10-1.c
new file mode 100644
index 000000000..9754abe1d
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-1.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep10-1.yml b/svcomp/reducercommutativity/sep10-1.yml
new file mode 100644
index 000000000..950f40085
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep10_false-def-behavior.i
+input_files: 'sep10-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep10-2.c b/svcomp/reducercommutativity/sep10-2.c
new file mode 100644
index 000000000..357be51a4
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-2.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep10-2.yml b/svcomp/reducercommutativity/sep10-2.yml
new file mode 100644
index 000000000..b990fbf8c
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep10_true-unreach-call.i
+input_files: 'sep10-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep20-1.c b/svcomp/reducercommutativity/sep20-1.c
new file mode 100644
index 000000000..9fb6dd3ac
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-1.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep20-1.yml b/svcomp/reducercommutativity/sep20-1.yml
new file mode 100644
index 000000000..8e524c46b
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep20_true-unreach-call.i
+input_files: 'sep20-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep20-2.c b/svcomp/reducercommutativity/sep20-2.c
new file mode 100644
index 000000000..7cefca3ab
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-2.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep20-2.yml b/svcomp/reducercommutativity/sep20-2.yml
new file mode 100644
index 000000000..94cbd8da5
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep20_false-def-behavior.i
+input_files: 'sep20-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep40-1.c b/svcomp/reducercommutativity/sep40-1.c
new file mode 100644
index 000000000..20d190511
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-1.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep40-1.yml b/svcomp/reducercommutativity/sep40-1.yml
new file mode 100644
index 000000000..e786d0df4
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep40_true-unreach-call.i
+input_files: 'sep40-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep40-2.c b/svcomp/reducercommutativity/sep40-2.c
new file mode 100644
index 000000000..6375eaa83
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-2.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep40-2.yml b/svcomp/reducercommutativity/sep40-2.yml
new file mode 100644
index 000000000..2fb3809b9
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep40_false-def-behavior.i
+input_files: 'sep40-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep60-1.c b/svcomp/reducercommutativity/sep60-1.c
new file mode 100644
index 000000000..588bf810c
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-1.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep60-1.yml b/svcomp/reducercommutativity/sep60-1.yml
new file mode 100644
index 000000000..022e141c8
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep60_false-def-behavior.i
+input_files: 'sep60-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep60-2.c b/svcomp/reducercommutativity/sep60-2.c
new file mode 100644
index 000000000..9c4fd1b59
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-2.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep60-2.yml b/svcomp/reducercommutativity/sep60-2.yml
new file mode 100644
index 000000000..2d2f6ea7f
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep60_true-unreach-call.i
+input_files: 'sep60-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum.c b/svcomp/reducercommutativity/sum.c
new file mode 100644
index 000000000..ffc23ea3b
--- /dev/null
+++ b/svcomp/reducercommutativity/sum.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum.yml b/svcomp/reducercommutativity/sum.yml
new file mode 100644
index 000000000..c5c94860f
--- /dev/null
+++ b/svcomp/reducercommutativity/sum.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sum_true-unreach-call_true-termination.i
+input_files: 'sum.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum05-1.c b/svcomp/reducercommutativity/sum05-1.c
new file mode 100644
index 000000000..501a6d31f
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum05-1.yml b/svcomp/reducercommutativity/sum05-1.yml
new file mode 100644
index 000000000..bc5f29e6c
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum05_false-def-behavior.i
+input_files: 'sum05-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum05-2.c b/svcomp/reducercommutativity/sum05-2.c
new file mode 100644
index 000000000..7937bee9e
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum05-2.yml b/svcomp/reducercommutativity/sum05-2.yml
new file mode 100644
index 000000000..344476f4d
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-2.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sum05_true-unreach-call_true-termination.i
+input_files: 'sum05-2.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum10-1.c b/svcomp/reducercommutativity/sum10-1.c
new file mode 100644
index 000000000..6e6cc0d80
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum10-1.yml b/svcomp/reducercommutativity/sum10-1.yml
new file mode 100644
index 000000000..91cf625c2
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sum10_true-unreach-call_true-termination.i
+input_files: 'sum10-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum10-2.c b/svcomp/reducercommutativity/sum10-2.c
new file mode 100644
index 000000000..06941d8ef
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum10-2.yml b/svcomp/reducercommutativity/sum10-2.yml
new file mode 100644
index 000000000..f64395959
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum10_false-def-behavior.i
+input_files: 'sum10-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum20-1.c b/svcomp/reducercommutativity/sum20-1.c
new file mode 100644
index 000000000..9fb3fa08e
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum20-1.yml b/svcomp/reducercommutativity/sum20-1.yml
new file mode 100644
index 000000000..6945ab778
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum20_false-def-behavior.i
+input_files: 'sum20-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum20-2.c b/svcomp/reducercommutativity/sum20-2.c
new file mode 100644
index 000000000..ced6c5d1f
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum20-2.yml b/svcomp/reducercommutativity/sum20-2.yml
new file mode 100644
index 000000000..be488b579
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sum20_true-unreach-call.i
+input_files: 'sum20-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum40-1.c b/svcomp/reducercommutativity/sum40-1.c
new file mode 100644
index 000000000..dccb3ed8f
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum40-1.yml b/svcomp/reducercommutativity/sum40-1.yml
new file mode 100644
index 000000000..8bcf00bc9
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum40_false-def-behavior.i
+input_files: 'sum40-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum40-2.c b/svcomp/reducercommutativity/sum40-2.c
new file mode 100644
index 000000000..63a47cd7c
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum40-2.yml b/svcomp/reducercommutativity/sum40-2.yml
new file mode 100644
index 000000000..d00fa60aa
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sum40_true-unreach-call.i
+input_files: 'sum40-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum60-1.c b/svcomp/reducercommutativity/sum60-1.c
new file mode 100644
index 000000000..8417b95a1
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum60-1.yml b/svcomp/reducercommutativity/sum60-1.yml
new file mode 100644
index 000000000..d8ab00da6
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum60_false-def-behavior.i
+input_files: 'sum60-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum60-2.c b/svcomp/reducercommutativity/sum60-2.c
new file mode 100644
index 000000000..a40f4bc5b
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum60-2.yml b/svcomp/reducercommutativity/sum60-2.yml
new file mode 100644
index 000000000..c04773efc
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sum60_true-unreach-call.i
+input_files: 'sum60-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
--
GitLab