Merge pull request #5933 from tautschnig/regression-tests-simplify

Enable goto-analyzer-simplify regression tests

Author: martin-cs

regression/CMakeLists.txt

@@ -49,6 +49,7 @@ add_subdirectory(goto-cc-cbmc)
 add_subdirectory(goto-cc-cbmc-shared-options)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
+add_subdirectory(goto-analyzer-simplify)
 add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)

regression/Makefile

@@ -24,6 +24,7 @@ DIRS = cbmc \
        goto-cc-cbmc-shared-options \
        cbmc-cpp \
        goto-cc-goto-analyzer \
+       goto-analyzer-simplify \
        statement-list \
        systemc \
        contracts \

regression/goto-analyzer-simplify/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-analyzer>"
+)

regression/goto-analyzer-simplify/Makefile

@@ -1,22 +1,15 @@
-
 default: tests.log
 
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
-		../failed-tests-printer.pl ; \
-		exit 1; \
-	fi
+	@../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer"
 
-tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
-		../failed-tests-printer.pl ; \
-		exit 1; \
-	fi
+tests.log: ../test.pl
+	@../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer"
 
 show:
 	@for dir in *; do \
 		if [ -d "$$dir" ]; then \
-			vim -o "$$dir/*.c" "$$dir/*.out"; \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
 		fi; \
 	done;
 

regression/goto-analyzer-simplify/chain.sh

@@ -1,14 +1,12 @@
 #!/bin/bash
 
-src_dir=../../../src
+set -e
 
-goto_analyzer=$src_dir/goto-analyzer/goto-analyzer
+goto_analyzer=$1
 
-options=$1
-file_name=${2%.c}
+options=${*:2:$#-2}
+name=${*:$#}
+name=${name%.c}
 
-echo options: $options
-echo file name : $file_name
-
-$goto_analyzer $file_name.c $options --simplify $file_name_simp.out
-$goto_analyzer $file_name_simp.out --show-goto-functions
+"${goto_analyzer}" "${name}.c" ${options} --simplify "${name}.gb"
+"${goto_analyzer}" "${name}.gb" --show-goto-functions

regression/goto-analyzer-simplify/partial-simplify-array/test.desc

@@ -1,5 +1,7 @@
 CORE
 main.c
-"--variable-sensitivity --vsd-arrays"
-
-arr\[0l\]
+--vsd --vsd-arrays every-element
+arr\[0l?l?\]
+^SIGNAL=0$
+^EXIT=0$
+--

regression/goto-analyzer-simplify/simplify-complex-expression/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
---variable-sensitivity
+--vsd
 r == 2
 ^SIGNAL=0$
-^EXIT=6$
+^EXIT=0$
 --
 --
 

regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc

@@ -1,7 +1,9 @@
 CORE
 main.c
-"--variable-sensitivity --vsd-arrays"
-
-arr\[0l\] =
-arr\[1l\] =
-arr\[\(signed long int\)nondet\] =
+--vsd --vsd-arrays every-element
+arr\[0l?l?\] =
+arr\[1l?l?\] =
+arr\[\(signed (long (long )?)?int\)nondet\] =
+^SIGNAL=0$
+^EXIT=0$
+--

regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
-"--variable-sensitivity --vsd-arrays --vsd-pointers"
-
+--vsd --vsd-arrays every-element --vsd-pointers value-set
 symbol_a = 1
 symbol_b = 2
-\*arr\[2l\] = 3;
-\*arr\[\(signed long int\)nondet_index\] = 4;
+\*arr\[2l?l?\] = 3;
+\*arr\[\(signed (long (long )?)?int\)nondet_index\] = 4;
+^SIGNAL=0$
+^EXIT=0$
+--

regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc

@@ -1,6 +1,8 @@
 CORE
 main.c
-"--variable-sensitivity --vsd-pointers"
-
+--vsd --vsd-pointers value-set
 symbol = 5
 \*pointer = 6
+^SIGNAL=0$
+^EXIT=0$
+--