diff --git a/AccessingCodebuildLogs.md b/AccessingCodebuildLogs.md deleted file mode 100644 index ca1a8976591..00000000000 --- a/AccessingCodebuildLogs.md +++ /dev/null @@ -1,30 +0,0 @@ -Accessing CodeBuild Logs ------------------------- - -The CodeBuild jobs on PRs can fail, but the logs have restricted access. - -To get hold of the logs you need to do the following: - -1. Get the job URL - -Right click on the relevant job, and copy the link URL - -![GetLink](doc/assets/GetLink.png) - -2. Extract the ID - -The link should look something like: - -> https://us-east-1.console.aws.amazon.com/codebuild/home?region=us-east-1#/builds/cbmc-linux-clang:*a32eddfe-19e6-45d9-b0e4-d9a92e5b5698*/view/new - -The job ID is the UID following the title of the job, int his case: - -> `a32eddfe-19e6-45d9-b0e4-d9a92e5b5698` - -3. Download the log - -Go to the following URL: - -http://cbmclogs.diffblue.com/{job-name}/{job-id}.gz - -Where `job-name` is the name of the job (e.g. `cbmc` or `cbmc-linux-clang`) and `job-id` is the ID extracted in the previous step. diff --git a/buildspec-linux-clang-3.8.yml b/buildspec-linux-clang-3.8.yml deleted file mode 100644 index a5a8813c1d4..00000000000 --- a/buildspec-linux-clang-3.8.yml +++ /dev/null @@ -1,28 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - apt-get update -y - - apt-get install -y clang-3.8 flex bison make git curl patch ccache libc6-dev-i386 jq openjdk-8-jdk maven - build: - commands: - - echo Build started on `date` - - make -C src minisat2-download - - make -C jbmc/src setup-submodules - - make -C src CXX='ccache /usr/bin/clang++-3.8' CXX_FLAGS='-Qunused-arguments -DDEBUG' - - make -C jbmc/src CXX='ccache /usr/bin/clang++-3.8' CXX_FLAGS='-Qunused-arguments -DDEBUG' - post_build: - commands: - - echo Build completed on `date` -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*' diff --git a/buildspec-linux-clang.yml b/buildspec-linux-clang.yml deleted file mode 100644 index ff790c8eb5c..00000000000 --- a/buildspec-linux-clang.yml +++ /dev/null @@ -1,44 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - runtime-versions: - java: openjdk8 - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - - - add-apt-repository 'deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-8 main' - - apt-get update -y - - apt-get install -y clang-8 flex bison make git curl patch ccache libc6-dev-i386 jq gdb - build: - commands: - - echo Build started on `date` - - make -C src minisat2-download - - make -C jbmc/src setup-submodules - - make -C src CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - - make -C unit CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - - make -C jbmc/src CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - - make -C jbmc/unit CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - post_build: - commands: - - make -C unit test - - echo "Running expected failure tests" - - make TAGS="[!shouldfail]" -C unit test - - make -C regression test CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' - - make -C regression/cbmc test-paths-lifo - - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - - make -C jbmc/unit test - - echo "Running expected failure tests" - - make TAGS="[!shouldfail]" -C jbmc/unit test - - make -C jbmc/regression test - - echo Build completed on `date` -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*' diff --git a/buildspec-linux-cmake-gcc.yml b/buildspec-linux-cmake-gcc.yml deleted file mode 100644 index 51ba6a538cf..00000000000 --- a/buildspec-linux-cmake-gcc.yml +++ /dev/null @@ -1,31 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - runtime-versions: - java: openjdk8 - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - apt-get update -y - - apt-get install -y flex bison make git curl patch ccache libc6-dev-i386 jq cmake - build: - commands: - - echo Build started on `date` - - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++' - - git submodule update --init --recursive - - cmake --build build -- -j2 - post_build: - commands: - - cd build; ctest -V -L CORE -j2 - - cd build; ctest -V -R unit-xfail -j2 - - echo Build completed on `date` -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*' diff --git a/buildspec-msbuild.yml b/buildspec-msbuild.yml deleted file mode 100644 index c53310981dd..00000000000 --- a/buildspec-msbuild.yml +++ /dev/null @@ -1,39 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - commands: - - choco install cyg-get -y --no-progress - - cyg-get bash patch bison flex make wget perl jq - - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 - - build: - commands: - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - bash -c "make -C src minisat2-download DOWNLOADER=wget" - - - | - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'bash -c "cd scripts ; ./generate_vcxproj"' - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C src BUILD_ENV=MSVC generated_files"' - $env:Path = "C:\Program Files (x86)\MSBuild\14.0\Bin;$env:Path" - msbuild /p:CLToolExe=clcache.exe /m:4 cbmc.vcxproj - - - | - # display cache stats - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'clcache -s' - -cache: - paths: - - 'c:\clcache\**\*' diff --git a/buildspec-windows-cmake.yml b/buildspec-windows-cmake.yml deleted file mode 100644 index a020571ca9c..00000000000 --- a/buildspec-windows-cmake.yml +++ /dev/null @@ -1,36 +0,0 @@ -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 cyg-get -y --no-progress - - cyg-get bison flex - - choco install -y --no-progress 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 -S . -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\**\*' diff --git a/buildspec-windows.yml b/buildspec-windows.yml deleted file mode 100644 index 47e8dc3c31c..00000000000 --- a/buildspec-windows.yml +++ /dev/null @@ -1,78 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - commands: - - choco install cyg-get -y --no-progress - - cyg-get bash patch bison flex make wget perl jq - - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 - - build: - commands: - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - bash -c "make -C src minisat2-download DOWNLOADER=wget" - - - | - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C src BUILD_ENV=MSVC" ' - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C unit all BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src setup-submodules" && bash -c "make CXX=clcache.exe -j4 -C jbmc/src BUILD_ENV=MSVC" ' - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C jbmc/unit all BUILD_ENV=MSVC" ' - - - | - # display cache stats - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'clcache -s' - - post_build: - commands: - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" ' - - - | - $env:Path = "$pwd\src\solvers;C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-cprover-smt2 BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C unit test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C jbmc/unit test BUILD_ENV=MSVC" ' - -cache: - paths: - - 'c:\clcache\**\*' diff --git a/buildspec.yml b/buildspec.yml deleted file mode 100644 index add9840d7fd..00000000000 --- a/buildspec.yml +++ /dev/null @@ -1,43 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - CP_EXTRA_CXXFLAGS: -D_GLIBCXX_DEBUG - -phases: - install: - runtime-versions: - java: openjdk8 - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - apt-get update -y - - apt-get install -y flex bison make git curl patch ccache libc6-dev-i386 jq gdb libxml2-utils - build: - commands: - - echo Build started on `date` - - make -C src minisat2-download - - make -C jbmc/src setup-submodules - - make -C src CXX="ccache g++" -j2 - - make -C unit CXX="ccache g++" -j2 - - make -C jbmc/src CXX="ccache g++" -j2 - - make -C jbmc/unit CXX="ccache g++" -j2 - post_build: - commands: - - make -C unit test - - echo "Running expected failure tests" - - make TAGS="[!shouldfail]" -C unit test - - make -C regression test - - make -C regression/cbmc test-paths-lifo - - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - - make -C jbmc/unit test - - echo "Running expected failure tests" - - make TAGS="[!shouldfail]" -C jbmc/unit test - - make -C jbmc/regression test - - echo Build completed on `date` -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*'