diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index b2a203c6349..edb9c4e257f 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -277,6 +277,59 @@ jobs: Set-Location build ctest -V -L CORE -C Release . -j2 + check-vs-2019-make-build-and-test: + runs-on: windows-2019 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + - name: Fetch dependencies + run: | + choco install winflexbison3 strawberryperl + nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 + echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH + echo "c:\ProgramData\chocolatey\bin" >> $env:GITHUB_PATH + echo "c:\Strawberry\" >> $env:GITHUB_PATH + - name: Setup MSBuild + uses: microsoft/setup-msbuild@v1.0.2 + - name: Initialise Developer Command Line + uses: ilammy/msvc-dev-cmd@v1 + - name: Prepare ccache + uses: actions/cache@v2 + with: + path: .ccache + key: ${{ runner.os }}-msbuild-make-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + ${{ runner.os }}-msbuild-make-${{ github.ref }} + ${{ runner.os }}-msbuild-make + - name: ccache environment + run: | + echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV + echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV + - name: Download minisat with make + run: make -C src minisat2-download + - name: Build CBMC with make + run: make CXX=clcache BUILD_ENV=MSVC -j2 -C src + - name: Build unit tests with make + run: make CXX=clcache BUILD_ENV=MSVC -j2 -C unit all + - name: Build jbmc with make + run: | + make CXX=clcache -j2 -C jbmc/src setup-submodules + make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/src + - name: Build JBMC unit tests + run: make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/unit all + - name: Print ccache stats + run: clcache -s + - name: Run CBMC and JBMC unit tests + run: | + make CXX=clcache BUILD_ENV=MSVC -C unit test + make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test + - name: Run CBMC regression tests + run: make CXX=clcache BUILD_ENV=MSVC -C regression test + + check-clang-format: runs-on: ubuntu-20.04 steps: diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile index 5df9faeb63a..01a91bcb2e0 100644 --- a/regression/cbmc-cpp/Makefile +++ b/regression/cbmc-cpp/Makefile @@ -4,7 +4,7 @@ include ../../src/config.inc include ../../src/common ifeq ($(BUILD_ENV_),MSVC) - excluded_tests = -X gcc-only + excluded_tests = -X gcc-only -X winbug else # In MacOS, a change in the assert.h header file # is causing template errors when exercising the diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile index 6d6d1753313..a940892af5d 100644 --- a/regression/cpp/Makefile +++ b/regression/cpp/Makefile @@ -10,7 +10,7 @@ else endif ifeq ($(BUILD_ENV_),MSVC) - excluded_tests = -X gcc-only + excluded_tests = -X gcc-only -X winbug else # In MacOS, a change in the assert.h header file # is causing template errors when exercising the diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile index cee41a751bd..8fbeca73e72 100644 --- a/regression/systemc/Makefile +++ b/regression/systemc/Makefile @@ -1,4 +1,17 @@ -ifneq ($(BUILD_ENV_),MSVC) +default: tests.log + +include ../../src/config.inc +include ../../src/common + +ifeq ($(BUILD_ENV_),MSVC) + exe = ../../../src/goto-cc/goto-cl +else + exe = ../../../src/goto-cc/goto-cc +endif + +ifeq ($(BUILD_ENV_),MSVC) + excluded_tests = -X gcc-only -X winbug +else # In MacOS, a change in the assert.h header file # is causing template errors when exercising the # C++ front end (because of a transitive include diff --git a/regression/test.pl b/regression/test.pl index 9a95233726d..650327401c9 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -76,7 +76,7 @@ ($$) my @data = grep { !/^\/\// } ; close FILE; - chomp @data; + s/\R$// for @data; if($exit_signal_checks) { grep { /^\^EXIT=[\(\|\d]*\d+\)?\$$/ } @data or die "$fname: Missing EXIT test\n"; grep { /^\^SIGNAL=\d+\$$/ } @data or die "$fname: Missing SIGNAL test\n"; diff --git a/src/common b/src/common index c597050a0d1..bb5b62d92df 100644 --- a/src/common +++ b/src/common @@ -146,11 +146,11 @@ ifeq ($(origin CXX),default) CXX = cl endif ifeq ($(origin YACC),default) - YACC = bison -y + YACC = win_bison -y endif YFLAGS ?= -v ifeq ($(origin LEX),default) - LEX = flex + LEX = win_flex endif