chg: start Gitlab CI configuration

.gitlab-ci.yml

@@ -0,0 +1,54 @@
+variables:
+  INSTALL_DIR: install
+  TCHECKER_BUILD_TYPE: Debug
+
+.build_and_test: &build_and_test
+  - ci-scripts/build.sh
+  - ci-scripts/test.sh
+
+.clang_conf: &clang_conf
+  stage: test
+  image: pictavien/tchecker-ci:clang-latest
+  variables:
+    CC : "clang"
+    CXX : "clang++"
+
+.gcc_conf: &gcc_conf
+  stage: test
+  image: pictavien/tchecker-ci:gcc-latest
+  variables:
+    CC : "gcc"
+    CXX : "g++"
+
+
+gcc_all_int32_no_memcheck:
+  <<: *gcc_conf
+  script:
+    - export CONFNAME="all:int32:no-memcheck"
+    - *build_and_test
+
+gcc_all_int16_no_memcheck:
+  <<: *gcc_conf
+  script:
+    - export CONFNAME="all:int16:no-memcheck"
+    - *build_and_test
+
+gcc_all_int64_memcheck:
+  <<: *gcc_conf
+  script:
+    - export CONFNAME="covreach:int64:memcheck"
+    - *build_and_test
+
+gcc_simplest_int32_memcheck:
+  <<: *gcc_conf
+  script:
+    - export CONFNAME="smallest:int32:memcheck"
+    - *build_and_test
+
+clang_all_int32_no_memcheck:
+  <<: *clang_conf
+  script:
+    - export CONFNAME="all:int32:no-memcheck"
+    - *build_and_test
+
+

ci-scripts/build.sh

@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+
+if ! test -z "${DEBUG_BUILD}"; then
+  set -v
+fi
+
+set -eu
+
+
+nbbits="32"
+memcheck="OFF"
+covreach="OFF"
+explore="OFF"
+unittests="OFF"
+simple_nr="OFF"
+bugfixes="OFF"
+
+if test -z "${CONFNAME}"; then
+  echo "Empty CONFNAME variable"
+  exit 1
+fi
+
+echo "Build tchecker for configuration: ${CONFNAME}"
+
+for cfgopt in $(sed -e 's/:/ /g' <<< "${CONFNAME}"); do
+  case "${cfgopt}" in
+    "int16"|"int32"|"int64")
+      nbbits=${cfgopt/int/}
+      ;;
+    "memcheck")
+      memcheck="ON"
+      ;;
+    "covreach")
+      covreach="ON"
+      ;;
+    "explore")
+      explore="ON"
+      ;;
+    "all")
+      covreach="ON"; explore="ON"; unittests="ON"; simple_nr="ON"; bugfixes="ON"
+      ;;
+    "smallest")
+      unittests="ON"; simple_nr="ON"; bugfixes="ON"
+      ;;
+  esac
+done
+
+TEST_CONF="-DUSEINT${nbbits}=ON"
+TEST_CONF="${TEST_CONF} -DTCK_ENABLE_MEMCHECK_TESTS=${memcheck}"
+TEST_CONF="${TEST_CONF} -DTCK_ENABLE_COVREACH_TESTS=${covreach}"
+TEST_CONF="${TEST_CONF} -DTCK_ENABLE_EXPLORE_TESTS=${explore}"
+TEST_CONF="${TEST_CONF} -DTCK_ENABLE_UNITTESTS=${unittests}"
+TEST_CONF="${TEST_CONF} -DTCK_ENABLE_SIMPLE_NR_TESTS=${simple_nr}"
+TEST_CONF="${TEST_CONF} -DTCK_ENABLE_BUGFIXES_TESTS=${bugfixes}"
+
+echo "TEST_CONF=${TEST_CONF}"
+
+mkdir build || true
+cd build
+cmake -DCMAKE_INSTALL_PREFIX=${INSTALL_DIR} \
+      -DCMAKE_CXX_COMPILER=${CXX} \
+      -DCMAKE_BUILD_TYPE=${TCHECKER_BUILD_TYPE} \
+      ${TEST_CONF} \
+      ..
+
+NB_CPUS=$(getconf _NPROCESSORS_CONF)
+exec make -j ${NB_CPUS}
+

ci-scripts/install-linux.sh

@@ -2,11 +2,6 @@
 
 set -eu
 
-if [ "${TRAVIS_OS_NAME}" != linux ]; then
-    echo "Not a Linux build; skipping installation"
-    exit 0
-fi
-
 $(dirname $0)/install-sources.sh
 
 

ci-scripts/install-sources.sh

@@ -4,10 +4,10 @@ set -eu
 
 echo "#### INSTALLING Catch2"
 
-git clone --branch ${CATCH2_BRANCH} https://github.com/catchorg/Catch2.git ${CATCH2_REPO} || true
-mkdir -p ${CATCH2_REPO}/build || true
+git clone --branch ${CATCH2_BRANCH} ${CATCH2_REPO_URL} ${CATCH2_DIRECTORY} || true
+mkdir -p ${CATCH2_DIRECTORY}/build || true
 
-pushd ${CATCH2_REPO}/build
+pushd ${CATCH2_DIRECTORY}/build
  cmake -DCMAKE_INSTALL_PREFIX=${INSTALL_DIR} ..
  make -j ${NB_CPUS}
  make install

ci-scripts/test.sh

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+
+set -euv
+
+NB_CPUS=$(getconf _NPROCESSORS_CONF)
+CTEST_PARALLEL_LEVEL=${NB_CPUS} CTEST_OUTPUT_ON_FAILURE=1 make -C build test
+

cmake/CheckCompilerFlags.cmake

@@ -6,13 +6,13 @@ include(CheckCXXCompilerFlag)
 
 # Options to support 16/32/64 bit dbm's
 # 32 is default
-option(USE16 "Use 16bit int" OFF)
-option(USE64 "Use 64bit int" OFF)
+option(USEINT16 "Use 16bit int" OFF)
+option(USEINT64 "Use 64bit int" OFF)
 
 set(INTEGER_T_SIZE 32)
-if (USE16)
+if (USEINT16)
     set(INTEGER_T_SIZE 16)
-elseif(USE64)
+elseif(USEINT64)
     set(INTEGER_T_SIZE 64)
 else()
 endif()

test/covreach/CMakeLists.txt

@@ -30,12 +30,12 @@ set(INPUTS
     train_gate.sh:3
     )
 
-if(NOT USE16)
+if(NOT USEINT16)
     list(APPEND INPUTS
          ad94_mid.sh:)
 endif()
 
-if(USE64)
+if(USEINT64)
     list(APPEND INPUTS
          ad94_Long.sh:)
 endif()
@@ -46,10 +46,10 @@ set(MEMCHECKED_TEST_REGEX
     "^.*ad94_[0-9].*raw.*$"
     "^.*critical-region-async.*raw.*$")
 
-if(USE16)
+if(USEINT16)
     list(APPEND MEMCHECKED_TEST_REGEX
          "^.*ad94_[0-9].*raw.*$")
-elseif(USE64)
+elseif(USEINT64)
     list(APPEND MEMCHECKED_TEST_REGEX
          "^.*ad94_Long.*raw.*$")
 else()

test/explore/CMakeLists.txt

@@ -19,12 +19,12 @@ set(INPUTS
     train_gate.sh:3
     )
 
-if(NOT USE16)
+if(NOT USEINT16)
     list(APPEND INPUTS
          ad94_mid.sh:)
 endif()
 
-if(USE64)
+if(USEINT64)
     list(APPEND INPUTS
          ad94_Long.sh:)
 endif()