Testing commit

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/Makefile

@@ -30,7 +30,6 @@ DIRS = cbmc \
 ifeq ($(WITH_MEMORY_ANALYZER),1)
   DIRS += snapshot-harness \
           memory-analyzer
-          # Empty last line
 endif
 
 # Run all test directories in sequence

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