diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 1fc45854947..c8b8382526f 100644 --- a/regression/CMakeLists.txt +++ b/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) diff --git a/regression/Makefile b/regression/Makefile index c4ec50d703f..9cc13313e34 100644 --- a/regression/Makefile +++ b/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 \ diff --git a/regression/goto-analyzer-simplify/CMakeLists.txt b/regression/goto-analyzer-simplify/CMakeLists.txt new file mode 100644 index 00000000000..d0e80bbd2bf --- /dev/null +++ b/regression/goto-analyzer-simplify/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $" +) diff --git a/regression/goto-analyzer-simplify/Makefile b/regression/goto-analyzer-simplify/Makefile index 9263df106d4..c94db202865 100644 --- a/regression/goto-analyzer-simplify/Makefile +++ b/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; diff --git a/regression/goto-analyzer-simplify/chain.sh b/regression/goto-analyzer-simplify/chain.sh index 5fbf28733ed..34c3aeac0fe 100755 --- a/regression/goto-analyzer-simplify/chain.sh +++ b/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 diff --git a/regression/goto-analyzer-simplify/partial-simplify-array/test.desc b/regression/goto-analyzer-simplify/partial-simplify-array/test.desc index 7c0b5afe8c1..a31ed037526 100644 --- a/regression/goto-analyzer-simplify/partial-simplify-array/test.desc +++ b/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$ +-- diff --git a/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc b/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc index 2e489c2332f..40eb8d1a1b4 100644 --- a/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc +++ b/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$ -- -- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc index 8ce04ba76ef..d1161d20eff 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc +++ b/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$ +-- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc index 4129ec58d45..715e8782c58 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc +++ b/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$ +-- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc index bc05dc76913..e7dc545e387 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc +++ b/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$ +-- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc index ea66f6e269a..e9181e3e47a 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc @@ -1,8 +1,10 @@ CORE main.c -"--variable-sensitivity --vsd-arrays --vsd-pointers --vsd-structs" - +--vsd --vsd-arrays every-element --vsd-pointers value-set --vsd-structs every-field symbol = 5 \*value\.pointer_component = 6 -value\.array\[1l\] = 2 -value\.array\[\(signed long int\)nondet\] = 3 +value\.array\[1l?l?\] = 2 +value\.array\[\(signed (long (long )?)?int\)nondet\] = 3 +^SIGNAL=0$ +^EXIT=0$ +-- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc index c2903b287f7..f5bb0f7c897 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc @@ -1,6 +1,9 @@ CORE main.c -"--variable-sensitivity --vsd-arrays --vsd-pointers" -array\[0l\] = 5 -array\[\(signed long int\)nondet\] = 6 -new_array\[1l\] = 7 +--vsd --vsd-arrays every-element --vsd-pointers value-set +array\[0l?l?\] = 5 +array\[\(signed (long (long )?)?int\)nondet\] = 6 +new_array\[1l?l?\] = 7 +^SIGNAL=0$ +^EXIT=0$ +-- diff --git a/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc b/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc index 6675045b32a..59ae86c6ccf 100644 --- a/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc +++ b/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc @@ -1,11 +1,11 @@ CORE main.c -"--variable-sensitivity" +--vsd ^SIGNAL=0$ -^EXIT=6$ +^EXIT=0$ main#return_value = 0; -- -- Tests that a multiplication of variable*variable can be simplified -if one of the variables can be evaluated to 0. \ No newline at end of file +if one of the variables can be evaluated to 0.