Merge pull request #5855 from NlightNFotis/port-msbuild-make-job

[CI] Add a make + windows github action job.

Author: NlightNFotis

.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/[email protected]
+      - 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:

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

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

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

regression/test.pl

@@ -76,7 +76,7 @@ ($$)
   my @data = grep { !/^\/\// } <FILE>;
   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";

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