Skip to content

Commit 97c830e

Browse files
NathanJPhillipsNathanJPhillips
authored
Merge pull request diffblue#243 from diffblue/pull-support-20171019
Pull latest cbmc/develop
2 parents caeef88 + e0c1c72 commit 97c830e

File tree

780 files changed

+7245
-2544
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

780 files changed

+7245
-2544
lines changed

‎CMakeLists.txt

Lines changed: 8 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -52,25 +52,18 @@ set(enable_cbmc_tests off CACHE BOOL "Whether CBMC tests should be enabled (the
5252
################################################################################
5353
# BOOST
5454

55-
set(boost_include_root_dir "${CMAKE_CURRENT_SOURCE_DIR}/cbmc/boost-include" )
56-
set(boost_include_package_download_dir "${boost_include_root_dir}/download" )
57-
set(boost_include_package_name "boost_1.63_headers.tar.bz2" )
5855
set(boost_include_package_URL "http://storage.googleapis.com/diffblue-mirror/boost/boost_1.63_headers.tar.bz2?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1542631994&Signature=X2GwPSm1dR8IPGP0D5JoyDmOnL%2Br4F7AI7NUA7SbmOAowMC0JS7Q5A6%2BkQziUzQa88zpddr5gSRbDOLqdoGzwLrYgPNtURS5dJ7l1q6xfJWSS%2FYf8be%2FSbdfLVN8qcXKCsfDe05Hqf%2Bz2cksqjQ1H6L0syj43rftbW4%2F7tp355%2BkinCeE466ulJeyru3CK%2F3RGX2Ul6ZQV6lNxkit1m6QM5BRtLbUQ1GOW0GCK9fWH2fry2n7kRVBCM3oz8fX62kLdKYlaXCf%2BvvXs9hOOmcQurL%2Fa4DCJYoClX%2BpznqXVmjUY%2FI3pD4HlRKbCeiPnoC6de2i1uxFNSVTBpG3w%2BtfA%3D%3D" )
59-
set(boost_include_include_dir "${boost_include_root_dir}")
60-
if (NOT EXISTS "${boost_include_package_download_dir}/${boost_include_package_name}")
61-
file(DOWNLOAD "${boost_include_package_URL}" "${boost_include_package_download_dir}/${boost_include_package_name}")
62-
endif()
6356

64-
include(ExternalProject)
65-
ExternalProject_Add(boost-include
66-
PREFIX "${boost_include_root_dir}"
67-
SOURCE_DIR "${boost_include_include_dir}/boost"
68-
URL "${boost_include_package_download_dir}/${boost_include_package_name}"
69-
CONFIGURE_COMMAND ""
70-
BUILD_COMMAND ""
71-
INSTALL_COMMAND ""
57+
include("${CMAKE_CURRENT_SOURCE_DIR}/cbmc/cmake/DownloadProject.cmake")
58+
59+
download_project(PROJ boost-include
60+
URL ${boost_include_package_URL}
61+
DOWNLOAD_NAME boost_1.63_headers.tar.bz2
62+
SOURCE_DIR ${CMAKE_BINARY_DIR}/boost-include-src/boost
7263
)
7364

65+
set(boost_include_include_dir ${boost-include_SOURCE_DIR}/..)
66+
7467
################################################################################
7568

7669
add_subdirectory(cbmc)

‎benchmarks/TRAINING/diffblue/taint_traces_01_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
{
1818
"error_traces":
1919
{
20-
"cbmc":
20+
"jbmc":
2121
[
2222
"search_for_error_traces/error_trace_0.json"
2323
],

‎benchmarks/TRAINING/diffblue/taint_traces_04_evaluator.json

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
[
1717
{
1818
"error_traces": {
19-
"cbmc": [
19+
"jbmc": [
2020
"search_for_error_traces/error_trace_0.json"
2121
],
2222
"symex": []
@@ -28,7 +28,7 @@
2828
},
2929
{
3030
"error_traces": {
31-
"cbmc": [
31+
"jbmc": [
3232
"search_for_error_traces/error_trace_1.json"
3333
],
3434
"symex": []
@@ -40,7 +40,7 @@
4040
},
4141
{
4242
"error_traces": {
43-
"cbmc": [
43+
"jbmc": [
4444
"search_for_error_traces/error_trace_2.json"
4545
],
4646
"symex": []

‎benchmarks/TRAINING/diffblue/taint_traces_05_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
[
1717
{
1818
"error_traces": {
19-
"cbmc": [
19+
"jbmc": [
2020
"search_for_error_traces/error_trace_0.json"
2121
],
2222
"symex": []

‎benchmarks/TRAINING/diffblue/taint_traces_06_evaluator.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
[
1717
{
1818
"error_traces": {
19-
"cbmc": [
19+
"jbmc": [
2020
"search_for_error_traces/error_trace_0.json"
2121
],
2222
"symex": []
@@ -28,7 +28,7 @@
2828
},
2929
{
3030
"error_traces": {
31-
"cbmc": [
31+
"jbmc": [
3232
"search_for_error_traces/error_trace_1.json"
3333
],
3434
"symex": []

‎benchmarks/TRAINING/diffblue/taint_traces_07_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
[
1717
{
1818
"error_traces": {
19-
"cbmc": [
19+
"jbmc": [
2020
"search_for_error_traces/error_trace_0.json"
2121
],
2222
"symex": []

‎benchmarks/evaluator.py

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ def __compare_computed_and_expected_results(error_traces, record):
119119
file_line = expected_loc_traces["file"] + "', line " + str(expected_loc_traces["line"])
120120
if not loc_traces:
121121
return "There are missing error traces for the sink location '" + file_line + "."
122-
if len(expected_loc_traces["error_traces"]["cbmc"]) != len(loc_traces["error_traces"]["cbmc"]):
122+
if len(expected_loc_traces["error_traces"]["jbmc"]) != len(loc_traces["error_traces"]["jbmc"]):
123123
return "Wrong number of CBMC generated error traces for the sink location '" + file_line + "."
124124
if len(expected_loc_traces["error_traces"]["symex"]) != len(loc_traces["error_traces"]["symex"]):
125125
return "Wrong number of SYMEX generated error traces for the sink location '" + file_line + "."
@@ -212,7 +212,7 @@ def __main():
212212
print("PASSED:\"" + benchmark["sources-dir"] + "\"")
213213
return 0 # success (for Travis)
214214
except Exception as e:
215-
print("ERROR: " + str(e))
215+
print("ERROR: " + repr(e))
216216
return 1 # failure (for Travis)
217217
except:
218218
print("ERROR: Unknown exception was raised.")

‎cbmc/CODING_STANDARD.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,11 @@ Here a few minimalistic coding rules for the CPROVER source tree.
182182
- Avoid `assert`. If the condition is an actual invariant, use INVARIANT,
183183
PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If
184184
there are possible reasons why it might fail, throw an exception.
185+
- All raw pointers (such as those returned by `symbol_tablet::lookup`) are
186+
assumed to be non-owning, and should not be `delete`d. Raw pointers that
187+
point to heap-allocated memory should be private data members of an object
188+
which safely manages the pointer. As such, `new` should only be used in
189+
constructors, and `delete` in destructors. Never use `malloc` or `free`.
185190

186191
# Architecture-specific code
187192
- Avoid if possible.

‎cbmc/cmake/DownloadProject.CMakeLists.cmake.in

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# Distributed under the OSI-approved MIT License. See accompanying
2+
# file LICENSE or https://github.com/Crascit/DownloadProject for details.
3+
4+
cmake_minimum_required(VERSION 2.8.2)
5+
6+
project(${DL_ARGS_PROJ}-download NONE)
7+
8+
include(ExternalProject)
9+
ExternalProject_Add(${DL_ARGS_PROJ}-download
10+
${DL_ARGS_UNPARSED_ARGUMENTS}
11+
SOURCE_DIR "${DL_ARGS_SOURCE_DIR}"
12+
BINARY_DIR "${DL_ARGS_BINARY_DIR}"
13+
CONFIGURE_COMMAND ""
14+
BUILD_COMMAND ""
15+
INSTALL_COMMAND ""
16+
TEST_COMMAND ""
17+
)

‎cbmc/cmake/DownloadProject.cmake

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
# Distributed under the OSI-approved MIT License. See accompanying
2+
# file LICENSE or https://github.com/Crascit/DownloadProject for details.
3+
#
4+
# MODULE: DownloadProject
5+
#
6+
# PROVIDES:
7+
# download_project( PROJ projectName
8+
# [PREFIX prefixDir]
9+
# [DOWNLOAD_DIR downloadDir]
10+
# [SOURCE_DIR srcDir]
11+
# [BINARY_DIR binDir]
12+
# [QUIET]
13+
# ...
14+
# )
15+
#
16+
# Provides the ability to download and unpack a tarball, zip file, git repository,
17+
# etc. at configure time (i.e. when the cmake command is run). How the downloaded
18+
# and unpacked contents are used is up to the caller, but the motivating case is
19+
# to download source code which can then be included directly in the build with
20+
# add_subdirectory() after the call to download_project(). Source and build
21+
# directories are set up with this in mind.
22+
#
23+
# The PROJ argument is required. The projectName value will be used to construct
24+
# the following variables upon exit (obviously replace projectName with its actual
25+
# value):
26+
#
27+
# projectName_SOURCE_DIR
28+
# projectName_BINARY_DIR
29+
#
30+
# The SOURCE_DIR and BINARY_DIR arguments are optional and would not typically
31+
# need to be provided. They can be specified if you want the downloaded source
32+
# and build directories to be located in a specific place. The contents of
33+
# projectName_SOURCE_DIR and projectName_BINARY_DIR will be populated with the
34+
# locations used whether you provide SOURCE_DIR/BINARY_DIR or not.
35+
#
36+
# The DOWNLOAD_DIR argument does not normally need to be set. It controls the
37+
# location of the temporary CMake build used to perform the download.
38+
#
39+
# The PREFIX argument can be provided to change the base location of the default
40+
# values of DOWNLOAD_DIR, SOURCE_DIR and BINARY_DIR. If all of those three arguments
41+
# are provided, then PREFIX will have no effect. The default value for PREFIX is
42+
# CMAKE_BINARY_DIR.
43+
#
44+
# The QUIET option can be given if you do not want to show the output associated
45+
# with downloading the specified project.
46+
#
47+
# In addition to the above, any other options are passed through unmodified to
48+
# ExternalProject_Add() to perform the actual download, patch and update steps.
49+
# The following ExternalProject_Add() options are explicitly prohibited (they
50+
# are reserved for use by the download_project() command):
51+
#
52+
# CONFIGURE_COMMAND
53+
# BUILD_COMMAND
54+
# INSTALL_COMMAND
55+
# TEST_COMMAND
56+
#
57+
# Only those ExternalProject_Add() arguments which relate to downloading, patching
58+
# and updating of the project sources are intended to be used. Also note that at
59+
# least one set of download-related arguments are required.
60+
#
61+
# If using CMake 3.2 or later, the UPDATE_DISCONNECTED option can be used to
62+
# prevent a check at the remote end for changes every time CMake is run
63+
# after the first successful download. See the documentation of the ExternalProject
64+
# module for more information. It is likely you will want to use this option if it
65+
# is available to you. Note, however, that the ExternalProject implementation contains
66+
# bugs which result in incorrect handling of the UPDATE_DISCONNECTED option when
67+
# using the URL download method or when specifying a SOURCE_DIR with no download
68+
# method. Fixes for these have been created, the last of which is scheduled for
69+
# inclusion in CMake 3.8.0. Details can be found here:
70+
#
71+
# https://gitlab.kitware.com/cmake/cmake/commit/bdca68388bd57f8302d3c1d83d691034b7ffa70c
72+
# https://gitlab.kitware.com/cmake/cmake/issues/16428
73+
#
74+
# If you experience build errors related to the update step, consider avoiding
75+
# the use of UPDATE_DISCONNECTED.
76+
#
77+
# EXAMPLE USAGE:
78+
#
79+
# include(DownloadProject)
80+
# download_project(PROJ googletest
81+
# GIT_REPOSITORY https://github.com/google/googletest.git
82+
# GIT_TAG master
83+
# UPDATE_DISCONNECTED 1
84+
# QUIET
85+
# )
86+
#
87+
# add_subdirectory(${googletest_SOURCE_DIR} ${googletest_BINARY_DIR})
88+
#
89+
#========================================================================================
90+
91+
92+
set(_DownloadProjectDir "${CMAKE_CURRENT_LIST_DIR}")
93+
94+
include(CMakeParseArguments)
95+
96+
function(download_project)
97+
98+
set(options QUIET)
99+
set(oneValueArgs
100+
PROJ
101+
PREFIX
102+
DOWNLOAD_DIR
103+
SOURCE_DIR
104+
BINARY_DIR
105+
# Prevent the following from being passed through
106+
CONFIGURE_COMMAND
107+
BUILD_COMMAND
108+
INSTALL_COMMAND
109+
TEST_COMMAND
110+
)
111+
set(multiValueArgs "")
112+
113+
cmake_parse_arguments(DL_ARGS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
114+
115+
# Hide output if requested
116+
if (DL_ARGS_QUIET)
117+
set(OUTPUT_QUIET "OUTPUT_QUIET")
118+
else()
119+
unset(OUTPUT_QUIET)
120+
message(STATUS "Downloading/updating ${DL_ARGS_PROJ}")
121+
endif()
122+
123+
# Set up where we will put our temporary CMakeLists.txt file and also
124+
# the base point below which the default source and binary dirs will be.
125+
# The prefix must always be an absolute path.
126+
if (NOT DL_ARGS_PREFIX)
127+
set(DL_ARGS_PREFIX "${CMAKE_BINARY_DIR}")
128+
else()
129+
get_filename_component(DL_ARGS_PREFIX "${DL_ARGS_PREFIX}" ABSOLUTE
130+
BASE_DIR "${CMAKE_CURRENT_BINARY_DIR}")
131+
endif()
132+
if (NOT DL_ARGS_DOWNLOAD_DIR)
133+
set(DL_ARGS_DOWNLOAD_DIR "${DL_ARGS_PREFIX}/${DL_ARGS_PROJ}-download")
134+
endif()
135+
136+
# Ensure the caller can know where to find the source and build directories
137+
if (NOT DL_ARGS_SOURCE_DIR)
138+
set(DL_ARGS_SOURCE_DIR "${DL_ARGS_PREFIX}/${DL_ARGS_PROJ}-src")
139+
endif()
140+
if (NOT DL_ARGS_BINARY_DIR)
141+
set(DL_ARGS_BINARY_DIR "${DL_ARGS_PREFIX}/${DL_ARGS_PROJ}-build")
142+
endif()
143+
set(${DL_ARGS_PROJ}_SOURCE_DIR "${DL_ARGS_SOURCE_DIR}" PARENT_SCOPE)
144+
set(${DL_ARGS_PROJ}_BINARY_DIR "${DL_ARGS_BINARY_DIR}" PARENT_SCOPE)
145+
146+
# The way that CLion manages multiple configurations, it causes a copy of
147+
# the CMakeCache.txt to be copied across due to it not expecting there to
148+
# be a project within a project. This causes the hard-coded paths in the
149+
# cache to be copied and builds to fail. To mitigate this, we simply
150+
# remove the cache if it exists before we configure the new project. It
151+
# is safe to do so because it will be re-generated. Since this is only
152+
# executed at the configure step, it should not cause additional builds or
153+
# downloads.
154+
file(REMOVE "${DL_ARGS_DOWNLOAD_DIR}/CMakeCache.txt")
155+
156+
# Create and build a separate CMake project to carry out the download.
157+
# If we've already previously done these steps, they will not cause
158+
# anything to be updated, so extra rebuilds of the project won't occur.
159+
# Make sure to pass through CMAKE_MAKE_PROGRAM in case the main project
160+
# has this set to something not findable on the PATH.
161+
configure_file("${_DownloadProjectDir}/DownloadProject.CMakeLists.cmake.in"
162+
"${DL_ARGS_DOWNLOAD_DIR}/CMakeLists.txt")
163+
execute_process(COMMAND ${CMAKE_COMMAND} -G "${CMAKE_GENERATOR}"
164+
-D "CMAKE_MAKE_PROGRAM:FILE=${CMAKE_MAKE_PROGRAM}"
165+
.
166+
RESULT_VARIABLE result
167+
${OUTPUT_QUIET}
168+
WORKING_DIRECTORY "${DL_ARGS_DOWNLOAD_DIR}"
169+
)
170+
if(result)
171+
message(FATAL_ERROR "CMake step for ${DL_ARGS_PROJ} failed: ${result}")
172+
endif()
173+
execute_process(COMMAND ${CMAKE_COMMAND} --build .
174+
RESULT_VARIABLE result
175+
${OUTPUT_QUIET}
176+
WORKING_DIRECTORY "${DL_ARGS_DOWNLOAD_DIR}"
177+
)
178+
if(result)
179+
message(FATAL_ERROR "Build step for ${DL_ARGS_PROJ} failed: ${result}")
180+
endif()
181+
182+
endfunction()
183+

‎cbmc/regression/CMakeLists.txt

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ macro(add_test_pl_profile name cmdline flag profile)
1010
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
1111
)
1212
set_tests_properties("${name}-${profile}" PROPERTIES
13-
LABELS "${profile}"
13+
LABELS "${profile};CBMC"
1414
)
1515
endmacro(add_test_pl_profile)
1616

@@ -35,6 +35,7 @@ add_subdirectory(goto-diff)
3535
add_subdirectory(goto-instrument)
3636
add_subdirectory(goto-instrument-typedef)
3737
add_subdirectory(invariants)
38+
add_subdirectory(jbmc-strings)
3839
add_subdirectory(strings)
3940
add_subdirectory(strings-smoke-tests)
4041
add_subdirectory(test-script)

‎cbmc/regression/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ DIRS = ansi-c \
55
cbmc-java-inheritance \
66
cpp \
77
goto-analyzer \
8+
goto-analyzer-taint \
89
goto-cc-cbmc \
910
goto-cc-goto-analyzer \
1011
goto-diff \
@@ -13,6 +14,7 @@ DIRS = ansi-c \
1314
goto-instrument-typedef \
1415
invariants \
1516
strings \
17+
jbmc-strings \
1618
strings-smoke-tests \
1719
test-script \
1820
# Empty last line

‎cbmc/regression/cbmc-java-inheritance/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:cbmc>"
2+
"$<TARGET_FILE:jbmc>"
33
)

‎cbmc/regression/cbmc-java-inheritance/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
default: tests.log
22

33
test:
4-
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
4+
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
55
../failed-tests-printer.pl ; \
66
exit 1 ; \
77
fi
88

99
tests.log: ../test.pl
10-
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
10+
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
1111
../failed-tests-printer.pl ; \
1212
exit 1 ; \
1313
fi

‎cbmc/regression/cbmc-java/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:cbmc>"
2+
"$<TARGET_FILE:jbmc>"
33
)

0 commit comments

Comments
 (0)