Native CMake support in VisualStudio

.gitignore

@@ -28,6 +28,7 @@ Release/*
 *.obj
 *.a
 *.lib
+src/ansi-c/converter_input.txt
 src/util/version.cpp
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc

CMakeLists.txt

@@ -1,5 +1,7 @@
 cmake_minimum_required(VERSION 3.2)
 
+project(CBMC)
+
 find_program(CCACHE_PROGRAM ccache)
 if(CCACHE_PROGRAM)
     set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
@@ -26,8 +28,17 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     #   Enable lots of warnings
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-    #   This would be the place to enable warnings for Windows builds, although
-    #   config.inc doesn't seem to do that currently
+    # This would be the place to enable warnings for Windows builds, although
+    # config.inc doesn't seem to do that currently
+
+    # Include Git Bash Environment (rqeuired for download_project (patch))
+    find_package(Git)
+    if(GIT_FOUND)
+        get_filename_component(git_root ${GIT_EXECUTABLE} DIRECTORY)
+        set(ENV{PATH} "${git_root}\\..\\usr\\bin;$ENV{PATH}")
+    else()
+        message(FATAL_ERROR "Git not found. Git bash is required to configure the build.")
+    endif()
 endif()
 
 set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")

buildspec-windows-cmake.yml

@@ -0,0 +1,34 @@
+version: 0.2
+
+env:
+  variables:
+    # CodeBuild console doesn't display color codes correctly
+    TESTPL_COLOR_OUTPUT: 0
+
+phases:
+  install:
+    commands:
+      - choco install -y --no-progress cmake --installargs 'ADD_CMAKE_TO_PATH=System'
+      - choco install -y --no-progress winflexbison3 ninja
+      - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
+
+  build:
+    commands:
+      - |
+        refreshenv
+        $Env:CLCACHE_DIR = "C:\clcache"
+        $Env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName
+        $Env:PATH = "C:\Program Files\CMake\bin;$Env:PATH"
+        $Env:PATH = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$Env:PATH"
+        & .\scripts\vcvars64.ps1
+        git submodule update --init --recursive
+        cmake "-H." -Bbuild -G Ninja "-DCMAKE_C_COMPILER=clcache.exe" "-DCMAKE_CXX_COMPILER=clcache.exe" -DCMAKE_BUILD_TYPE=Release
+        cmake --build build --config Release --target cbmc
+        cmake --build build --config Release --target jbmc
+        cmake --build build --config Release --target unit
+        # display cache stats
+        clcache -s
+
+cache:
+  paths:
+    - 'c:\clcache\**\*'

scripts/vcvars64.ps1

@@ -0,0 +1,14 @@
+# Set up environmental variables for building with Visual Studio 2015 x64
+#
+# Source:
+# https://stackoverflow.com/questions/2124753/how-can-i-use-powershell-with-the-visual-studio-command-prompt
+
+pushd 'C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC'    
+cmd /c "vcvarsall.bat&set" |
+foreach {
+  if ($_ -match "=") {
+    $v = $_.split("="); set-item -force -path "ENV:\$($v[0])"  -value "$($v[1])"
+  }
+}
+popd
+write-host "`nVisual Studio 2015 Command Prompt variables set." -ForegroundColor Yellow

src/ansi-c/CMakeLists.txt

@@ -4,15 +4,16 @@ generic_flex(ansi_c)
 add_executable(converter library/converter.cpp)
 
 file(GLOB ansi_c_library_sources "library/*.c")
-
-add_custom_command(OUTPUT converter_input.txt
-    COMMAND cat ${ansi_c_library_sources} > converter_input.txt
-    DEPENDS ${ansi_c_library_sources}
-)
+set(converter_input_path "${CMAKE_CURRENT_SOURCE_DIR}/converter_input.txt")
+file(WRITE ${converter_input_path} "")
+foreach(source ${ansi_c_library_sources})
+    file(READ ${source} file_contents)
+    file(APPEND ${converter_input_path} "${file_contents}")
+endforeach()
 
 add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
-    COMMAND converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
-    DEPENDS "converter_input.txt" converter
+    COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+    DEPENDS converter
 )
 
 add_executable(file_converter file_converter.cpp)