Perform memory regression test in Travis/Ubuntu/cmake/g++ build

The CMake build configuration is now set to RelWithDebInfo to obtain usable
function call names in the heap trace. As this yields different and larger
binaries, ccache's cache size is increased to 2G for this stage.

Author: tautschnig

Diff for: .travis.yml

@@ -182,7 +182,7 @@ jobs:
         - CCACHE_CPP2=yes
       script: echo "Not running any tests for a debug build."
 
-    # cmake build using g++-5
+    # cmake build using g++-5 + memory regression test
     - stage: Test different OS/CXX/Flags
       os: linux
       compiler: gcc
@@ -195,14 +195,24 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
+            - valgrind
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       install:
         - ccache -z
-        - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
+        - ccache --max-size=2G
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=RelWithDebInfo'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
         - cmake --build build -- -j4
-      script: (cd build; ctest -V -L CORE -j2)
+      env:
+        - NAME="memory-regression"
+      script:
+        - cd build && ctest -V -L CORE -j2 || exit 1
+        - valgrind --tool=massif --massif-out-file=massif.out --time-unit=B
+          bin/cbmc ../regression/cbmc/address_space_size_limit1/test.c
+          --no-simplify --unwind 300 --object-bits 8 || true
+        - if ! ../scripts/memory-test/memory.py
+          -r ../scripts/memory-test/massif.ref.x86-64 massif.out ; then
+          echo "Dumping massif.out" ; cat massif.out ; exit 1 ; fi
 
     - stage: Test different OS/CXX/Flags
       os: osx