Updates requested in the PR.

Author: marek-trtik

.travis.yml

@@ -162,7 +162,6 @@ jobs:
         - RUN_CBMC_TESTS="false"
         - RUN_SECURITY_TESTS="true"
         - CCACHE_CPP2=yes
-        - EXTRA_CXXFLAGS="-DDEBUG"
 
 
   allow_failures:

CMakeLists.txt

@@ -43,7 +43,7 @@ set(CMAKE_CXX_STANDARD_REQUIRED true)
 
 set(CMAKE_EXPORT_COMPILE_COMMANDS true)
 
-set(enable_security_tests off CACHE BOOL "Whether tests of the security analyser should be enabled.")
+set(enable_security_tests on CACHE BOOL "Whether tests of the security analyser should be enabled.")
 set(enable_cbmc_tests off CACHE BOOL "Whether CBMC tests should be enabled (the default is to enable just test-gen tests)")
 
 ################################################################################

security-analyser-driver.py

@@ -1,2 +1,2 @@
-# TODO: this script should only forwad its input to the driver script.
+# TODO: this script should only forwrad its input to the driver script.
 #       Implement it! Until then, this script is bypassed by the evaluator.

src/CMakeLists.txt

@@ -8,10 +8,11 @@ macro(generic_includes name)
         ${SECURITY_ANALYSER_SOURCE_DIR}
         ${CMAKE_CURRENT_BINARY_DIR}
         ${CMAKE_CURRENT_SOURCE_DIR}
+        ${CBMC_SOURCE_DIR}
+        ${boost_include_include_dir}
     )
 endmacro(generic_includes)
 
-add_definitions(-DUSE_BOOST)
 
 add_subdirectory(driver)
 add_subdirectory(pointer-analysis)

src/driver/CMakeLists.txt

@@ -21,12 +21,7 @@ endif()
 
 target_compile_definitions(security-analyzer
   PRIVATE "-DSECURITY_ANALYSER_VERSION=\"${git_repo_version}\""
-)
-
-target_include_directories(security-analyzer
-    PRIVATE
-    ${CBMC_SOURCE_DIR}
-    "${boost_include_include_dir}"
+          USE_BOOST=1
 )
 
 generic_includes(security-analyzer)

src/pointer-analysis/CMakeLists.txt

@@ -5,10 +5,8 @@ add_library(sec_pointer_analysis
     ${headers}
 )
 
-target_include_directories(sec_pointer_analysis
-    PRIVATE
-    ${CBMC_SOURCE_DIR}
-    "${boost_include_include_dir}"
+target_compile_definitions(sec_pointer_analysis
+  PRIVATE USE_BOOST=1
 )
 
 generic_includes(sec_pointer_analysis)

src/summaries/CMakeLists.txt

@@ -5,10 +5,8 @@ add_library(sec_summaries
     ${headers}
 )
 
-target_include_directories(sec_summaries
-    PRIVATE
-    ${CBMC_SOURCE_DIR}
-    "${boost_include_include_dir}"
+target_compile_definitions(sec_summaries
+  PRIVATE USE_BOOST=1
 )
 
 generic_includes(sec_summaries)

src/taint-analysis/CMakeLists.txt

@@ -5,10 +5,8 @@ add_library(sec_taint_analysis
     ${headers}
 )
 
-target_include_directories(sec_taint_analysis
-    PRIVATE
-    ${CBMC_SOURCE_DIR}
-    "${boost_include_include_dir}"
+target_compile_definitions(sec_taint_analysis
+  PRIVATE USE_BOOST=1
 )
 
 generic_includes(sec_taint_analysis)

src/taint-slicer/CMakeLists.txt

@@ -5,10 +5,8 @@ add_library(sec_taint_slicer
     ${headers}
 )
 
-target_include_directories(sec_taint_slicer
-    PRIVATE
-    ${CBMC_SOURCE_DIR}
-    "${boost_include_include_dir}"
+target_compile_definitions(sec_taint_slicer
+  PRIVATE USE_BOOST=1
 )
 
 generic_includes(sec_taint_slicer)

src/util/CMakeLists.txt

@@ -5,10 +5,8 @@ add_library(sec_util
     ${headers}
 )
 
-target_include_directories(sec_util
-    PRIVATE
-    ${CBMC_SOURCE_DIR}
-    "${boost_include_include_dir}"
+target_compile_definitions(sec_util
+  PRIVATE USE_BOOST=1
 )
 
 generic_includes(sec_util)

unit/range_union/CMakeLists.txt

@@ -3,8 +3,8 @@ file(GLOB_RECURSE headers "*.h")
 add_executable(test-union
     ${sources}
     ${headers}
-	../test.cpp
-	../indentation.cpp
+    ../test.cpp
+    ../indentation.cpp
 )
 
 target_include_directories(test-union

unit/serialization/CMakeLists.txt

@@ -3,9 +3,9 @@ file(GLOB_RECURSE headers "*.h")
 add_executable(test-serializer
     ${sources}
     ${headers}
-	../test.cpp
-	../indentation.cpp
-  taint-config.json
+    ../test.cpp
+    ../indentation.cpp
+    taint-config.json
 )
 
 target_include_directories(test-serializer