Fix memory-analyzer regression tests

The make-builds did not refer to the goto-gcc correctly. Also the result of
pointer_to_struct test change, but it is consistent now. And the gdb does not
seem to work on OSX so we skip that build in CI.

Author: petr-bauch

.travis.yml

@@ -284,7 +284,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64' '-DWITH_MEMORY_ANALYZER=On'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
@@ -330,16 +330,17 @@ install:
   - make -C src minisat2-download
   - make -C src/ansi-c library_check
   - make -C src/cpp library_check
-  - env WITH_MEMORY_ANALYZER=1 make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
+  - if [ $TRAVIS_OS_NAME=linux ] ; then env WITH_MEMORY_ANALYZER=1 ; fi ;
+  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-  - env UBSAN_OPTIONS=print_stacktrace=1 WITH_MEMORY_ANALYZER=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
-  - UBSAN_OPTIONS=print_stacktrace=1 WITH_MEMORY_ANALYZER=1 make -C regression/cbmc test-paths-lifo
-  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 WITH_MEMORY_ANALYZER=1 make -C regression/cbmc test-cprover-smt2
-  - env WITH_MEMORY_ANALYZER=1 make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
-  - env WITH_MEMORY_ANALYZER=1 make -C unit test
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
+  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
+  - env make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
+  - env make -C unit test
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C jbmc/unit test

regression/memory-analyzer/CMakeLists.txt

@@ -1,3 +1,4 @@
 add_test_pl_tests(
   "../chain.sh \
-   $<TARGET_FILE:memory-analyzer>")
+   $<TARGET_FILE:memory-analyzer> \
+   ../../../build/bin/goto-gcc")

regression/memory-analyzer/Makefile

@@ -1,7 +1,7 @@
 default: clean tests.log
 
-GOTO_GCC_EXE=../../../src/goto-cc/goto-gcc
 MEMORY_ANALYZER_EXE=../../../src/memory-analyzer/memory-analyzer
+GOTO_GCC_EXE=../../../src/goto-cc/goto-gcc
 
 clean:
 	find -name '*.exe' -execdir $(RM) '{}' \;

regression/memory-analyzer/chain.sh

@@ -2,7 +2,7 @@
 
 set -e
 
-#goto_gcc="../../../build/bin/goto-gcc"
+#goto_gcc=../../build/bin/goto-gcc
 memory_analyzer=$1
 goto_gcc=$2
 name=${*:$#}

regression/memory-analyzer/pointer_to_struct_01/test.desc

@@ -2,8 +2,7 @@ CORE
 main.exe
 --breakpoint checkpoint --symbols p
 struct S tmp;
-tmp = \{ \.next=\(\(struct S \*\)(NULL|0)\) \};
-p = &tmp;
-p->next = &tmp;
+tmp = \{ \.next=\(\(struct S \*\)0\) \};
+p = \&tmp;
 ^EXIT=0$
 ^SIGNAL=0$

src/Makefile

@@ -17,7 +17,6 @@ DIRS = analyses \
        json-symtab-language \
        langapi \
        linking \
-       memory-analyzer \
        pointer-analysis \
        solvers \
        util \
@@ -34,6 +33,7 @@ ALLDEPS = cbmc.dir \
 
 
 ifeq ($(WITH_MEMORY_ANALYZER),1)
+  DIRS += memory-analyzer
   ALLDEPS += memory-analyzer.dir
 endif