Skip to content

Commit bc887c5

Browse files
smowtonsmowton
committed
Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019
2 parents 9a59fb9 + 64d81f1 commit bc887c5

File tree

765 files changed

+7165
-2449
lines changed

Some content is hidden

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

765 files changed

+7165
-2449
lines changed

‎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.

‎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+
)

‎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+

‎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)

‎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

‎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
)

‎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

‎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
)

‎regression/cbmc-java/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

‎regression/cbmc-java/generics_symtab1/generics$bound_element.class

892 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)