Merge pull request #570 from zemanlx/feature/compile-on-musl

Support for non-glibc linux which use musl-libc

Author: Daniel Kroening

.travis.yml

@@ -1,10 +1,35 @@
 language: cpp
 
-sudo: false
-
 matrix:
   include:
+
+    # Alpine Linux with musl-libc using g++
+    - os: linux
+      sudo: required
+      compiler: gcc
+      services:
+        - docker
+      before_install:
+        - docker pull diffblue/cbmc-builder:alpine
+      env:
+        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc diffblue/cbmc-builder:alpine"
+        - COMPILER=g++
+
+    # OS X using g++
+    - os: osx
+      sudo: false
+      compiler: gcc
+      env: COMPILER=g++
+
+    # OS X using clang++
+    - os: osx
+      sudo: false
+      compiler: clang
+      env: COMPILER=clang++
+
+    # Ubuntu Linux with glibc using g++-5
     - os: linux
+      sudo: false
       compiler: gcc
       addons:
         apt:
@@ -18,7 +43,10 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER=g++-5
+
+    # Ubuntu Linux with glibc using clang++-3.7
     - os: linux
+      sudo: false
       compiler: clang
       addons:
         apt:
@@ -34,18 +62,17 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env: COMPILER=clang++-3.7
-    - os: osx
-      compiler: gcc
-      env: COMPILER=g++
-    - os: osx
-      compiler: clang
-      env: COMPILER=clang++
+
     - env: NAME="CPP-LINT"
       script: scripts/travis_lint.sh || true
 
 script:
   - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    make -C src minisat2-download &&
-    make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 &&
-    env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test &&
-    make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir
+    COMMAND="make -C src minisat2-download" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
+    eval ${PRE_COMMAND} ${COMMAND}

regression/cpp/enum8/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.cpp
-
+--std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --

scripts/minisat-2.2.1-patch

@@ -196,3 +196,15 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
 
      int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
      void operator ++ ()       { pos++; assureLookahead(); }
+diff -urN minisat-2.2.1/minisat/utils/System.h minisat-2.2.1.patched/minisat/utils/System.h
+--- minisat-2.2.1/minisat/utils/System.h	2017-02-21 18:23:22.727464369 +0000
++++ minisat-2.2.1.patched/minisat/utils/System.h	2017-02-21 18:23:14.451343361 +0000
+@@ -21,7 +21,7 @@
+ #ifndef Minisat_System_h
+ #define Minisat_System_h
+ 
+-#if defined(__linux__)
++#if defined(__linux__) && defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+ 

src/util/memory_info.cpp

@@ -39,7 +39,7 @@ Function: memory_info
 
 void memory_info(std::ostream &out)
 {
-  #ifdef __linux__
+  #if defined(__linux__) && defined(__GLIBC__)
   // NOLINTNEXTLINE(readability/identifiers)
   struct mallinfo m = mallinfo();
   out << "  non-mmapped space allocated from system: " << m.arena << "\n";