From c1b1d0719d93d498ac2c81bdedfa63f6c86a8f1f Mon Sep 17 00:00:00 2001
From: Yumi Bagge <yumi.bagge@diffblue.com>
Date: Thu, 23 May 2019 13:06:52 +0100
Subject: [PATCH 1/5] Add AWS CodeBuild spec to run codecov

---
 buildspec-linux-make-gcc-cov.yml | 46 ++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 buildspec-linux-make-gcc-cov.yml

diff --git a/buildspec-linux-make-gcc-cov.yml b/buildspec-linux-make-gcc-cov.yml
new file mode 100644
index 00000000000..32e8c632391
--- /dev/null
+++ b/buildspec-linux-make-gcc-cov.yml
@@ -0,0 +1,46 @@
+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 libwww-perl patch ccache libc6-dev-i386 jq gdb lcov curl python-pip
+      - pip install codecov
+  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 CPROVER_WITH_PROFILING=1
+      - make -C unit CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1
+      - make -C jbmc/src CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1
+      - make -C jbmc/unit CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1
+  post_build:
+    commands:
+      - make -C unit test 
+      - make -C regression test CPROVER_WITH_PROFILING=1
+      - 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
+      - make -C jbmc/regression test
+      - lcov --capture --directory . --output-file ./lcov.info
+      - VCS_PULL_REQUEST=$(echo $CODEBUILD_SOURCE_VERSION | sed 's/pr\///g')
+      - COV_SCRIPT=/root/.cache/codecov.sh
+      - if [ ! -f "$COV_SCRIPT" ]; then curl -s https://codecov.io/bash > "$COV_SCRIPT"; fi
+      - echo "$CODEBUILD_INITIATOR" | grep GitHub && bash "$COV_SCRIPT" -t "$CODECOV_TOKEN" || true      
+      - echo Build completed on `date`
+cache:
+  paths:
+    - '/var/cache/apt/**/*'
+    - '/var/lib/apt/lists/**/*'
+    - '/root/.ccache/**/*'
+    - '/root/.cache/codecov.sh'
+  
\ No newline at end of file

From 0ef5e78de9b17f42d86dc60a3afc2a0257235e90 Mon Sep 17 00:00:00 2001
From: Yumi Bagge <yumi.bagge@diffblue.com>
Date: Fri, 24 May 2019 14:01:21 +0100
Subject: [PATCH 2/5] Add CPROVER_WITH_PROFILING to make build

to be enabled for coverage measurement
---
 buildspec-linux-make-gcc-cov.yml | 1 -
 src/config.inc                   | 5 +++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/buildspec-linux-make-gcc-cov.yml b/buildspec-linux-make-gcc-cov.yml
index 32e8c632391..5bcbc52c81e 100644
--- a/buildspec-linux-make-gcc-cov.yml
+++ b/buildspec-linux-make-gcc-cov.yml
@@ -43,4 +43,3 @@ cache:
     - '/var/lib/apt/lists/**/*'
     - '/root/.ccache/**/*'
     - '/root/.cache/codecov.sh'
-  
\ No newline at end of file
diff --git a/src/config.inc b/src/config.inc
index c8114488f18..717faf4ed58 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -8,6 +8,11 @@ else
   CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum
 endif
 
+ifeq ($(CPROVER_WITH_PROFILING),1)
+  CXXFLAGS += -fprofile-arcs -ftest-coverage
+  LINKFLAGS += -lgcov -fprofile-arcs
+endif
+
 # Select optimisation or debug info
 #CXXFLAGS += -O2 -DNDEBUG
 #CXXFLAGS += -O0 -g

From 69dbdefcfa4189c521bf515f1de469500e284cc0 Mon Sep 17 00:00:00 2001
From: Yumi Bagge <yumi.bagge@diffblue.com>
Date: Thu, 30 May 2019 09:44:45 +0100
Subject: [PATCH 3/5] Add codecov badge

---
 README.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/README.md b/README.md
index fd4fb10f0f2..8c69317155c 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,7 @@
 ![Build Status][codebuild_img]
 ![Build Status][codebuild_windows_img]
 [![Build Status][coverity_img]][coverity]
+[![Build Status][codecov_img]][codecov]
 
 [CProver Wiki](http://www.cprover.org/wiki)
 
@@ -59,3 +60,5 @@ License
 [codebuild_windows_img]: https://codebuild.us-east-1.amazonaws.com/badges?uuid=eyJlbmNyeXB0ZWREYXRhIjoiTFQ4Q0lCSEc1Rk5NcmlzaFZDdU44Vk8zY0c1VCtIVWMwWnJMRitmVFI5bE94Q3dhekVPMWRobFU2Q0xTTlpDSWZUQ3J1eksrWW1rSll1OExXdll2bExZPSIsIml2UGFyYW1ldGVyU3BlYyI6InpqcloyaEdxbjBiQUtvNysiLCJtYXRlcmlhbFNldFNlcmlhbCI6MX0%3D&branch=develop
 [coverity]: https://scan.coverity.com/projects/diffblue-cbmc
 [coverity_img]: https://scan.coverity.com/projects/13552/badge.svg
+[codecov]: https://codecov.io/gh/diffblue/cbmc
+[codecov_img]: https://codecov.io/gh/diffblue/cbmc/branch/develop/graphs/badge.svg

From 0ea62e3f7b3dbce5b88919a24a64b34c9b2daa1f Mon Sep 17 00:00:00 2001
From: Yumi Bagge <yumi.bagge@diffblue.com>
Date: Thu, 30 May 2019 22:02:50 +0100
Subject: [PATCH 4/5] Add AWS CodeBuild spec to run codecov w cmake

This is not a part of CI.
---
 buildspec-linux-cmake-gcc-cov.yml | 37 +++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 buildspec-linux-cmake-gcc-cov.yml

diff --git a/buildspec-linux-cmake-gcc-cov.yml b/buildspec-linux-cmake-gcc-cov.yml
new file mode 100644
index 00000000000..bdb3e2d1372
--- /dev/null
+++ b/buildspec-linux-cmake-gcc-cov.yml
@@ -0,0 +1,37 @@
+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
+      - add-apt-repository ppa:ubuntu-toolchain-r/test
+      - apt-get update -y
+      - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq lcov cmake curl gdb python-pip
+      - pip install codecov
+  build:
+    commands:
+      - echo Build started on `date`
+      - git submodule update --init --recursive
+      - cmake -H. -Bbuild '-Denable_coverage=1' '-Dparallel_tests=2' '-DCMAKE_CXX_COMPILER=/usr/bin/g++'
+      - cmake --build build --target coverage -- -j2
+  post_build:
+    commands:
+      - lcov --capture --directory build --output-file ./lcov.info
+      - VCS_PULL_REQUEST=$(echo $CODEBUILD_SOURCE_VERSION | sed 's/pr\///g')
+      - COV_SCRIPT=/root/.cache/codecov.sh
+      - if [ ! -f "$COV_SCRIPT" ]; then curl -s https://codecov.io/bash > "$COV_SCRIPT"; fi
+      - echo "$CODEBUILD_INITIATOR" | grep GitHub && bash "$COV_SCRIPT" -t "$CODECOV_TOKEN" || true
+      - echo Build completed on `date`
+cache:
+  paths:
+    - '/var/cache/apt/**/*'
+    - '/var/lib/apt/lists/**/*'
+    - '/root/.ccache/**/*'
+    - '/root/.cache/codecov.sh'

From a780511db12c36c136c73a4819e48b2c0c9601b2 Mon Sep 17 00:00:00 2001
From: Yumi Bagge <yumi.bagge@diffblue.com>
Date: Thu, 30 May 2019 13:48:51 +0100
Subject: [PATCH 5/5] Add goto-harness dependency and unify format

---
 CMakeLists.txt | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 382032054ff..26732212843 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -88,7 +88,10 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
             COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --remove ${CODE_COVERAGE_INFO_FILE} '/usr/*' --output-file ${CODE_COVERAGE_INFO_FILE}
             COMMAND ${CODE_COVERAGE_GENHTML} ${CODE_COVERAGE_INFO_FILE} --output-directory ${CODE_COVERAGE_OUTPUT_DIR}
             DEPENDS
-              java-models-library java-unit unit
+              java-models-library
+              "$<TARGET_FILE:java-unit>"
+              "$<TARGET_FILE:unit>"
+              "$<TARGET_FILE:goto-harness>"
               "$<TARGET_FILE:cbmc>"
               "$<TARGET_FILE:driver>"
               "$<TARGET_FILE:goto-analyzer>"