Build jbmc on CI

peterschrammel · peterschrammel · commit 29a88185e8b3 · 2018-05-20T23:00:12.000+01:00
diff --git a/.travis.yml b/.travis.yml
@@ -248,7 +248,7 @@ jobs:
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "coverity-scan@diffblue.com"
           build_command_prepend: "make -C src minisat2-download"
-          build_command: "make -C src -j2"
+          build_command: "make -C src -j2; make -C jbmc/src -j2"
           branch_pattern: "develop"
       before_install:
         - |
@@ -277,12 +277,16 @@ install:
   - make -C src/ansi-c library_check
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
+  - 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 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - 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
 
 before_cache:
   - ccache -s
diff --git a/appveyor.yml b/appveyor.yml
@@ -53,11 +53,11 @@ build_script:
     call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64
     sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc
     make -C src -j2
+    make -C jbmc/src -j2
 
 test_script:
 - cmd: |
     cd regression
-
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
     rmdir /s /q ansi-c\arch_flags_mcpu_good
@@ -90,15 +90,24 @@ test_script:
     rmdir /s /q cpp\nullptr1
     rmdir /s /q cpp\sizeof1
     rmdir /s /q cpp\static_assert1
-    rmdir /s /q cbmc-java\VarLengthArrayTrace1
-    rmdir /s /q cbmc-java\classpath1
-    rmdir /s /q cbmc-java\jar-file3
-    rmdir /s /q cbmc-java\tableswitch2
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
+    cd ..
 
-    make test
+    make -C regression test
 
-    cd ..
-    make -C unit all
+    make -C unit all -j2
     make -C unit test
+
+    cd jbmc/regression
+    rmdir /s /q jbmc\VarLengthArrayTrace1
+    rmdir /s /q jbmc\classpath1
+    rmdir /s /q jbmc\jar-file3
+    rmdir /s /q jbmc\tableswitch2
+    rmdir /s /q jbmc-concurrency\explicit_thread_blocks
+    cd ../..
+
+    make -C jbmc/regression test
+
+    make -C jbmc/unit all -j2
+    make -C jbmc/unit test
