Skip to content

Commit 64d81f1

Browse files
committed
Merge remote-tracking branch 'upstream/develop' into pull-support-20171019
2 parents 9a59fb9 + 9e05177 commit 64d81f1

File tree

764 files changed

+7137
-2427
lines changed

Some content is hidden

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

764 files changed

+7137
-2427
lines changed

CODING_STANDARD.md

+5
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.
+17
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

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

+2-1
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

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

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

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

+2-2
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
Binary file not shown.
Binary file not shown.
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
public class generics {
2+
3+
class element<E> {
4+
E elem;
5+
}
6+
7+
class bound_element<NUM extends java.lang.Number> {
8+
NUM elem;
9+
NUM f() {
10+
return elem;
11+
}
12+
void g(NUM e) {
13+
elem=e;
14+
}
15+
}
16+
17+
bound_element<Integer> belem;
18+
19+
Integer f(int n) {
20+
21+
element<Integer> e=new element<>();
22+
e.elem=n;
23+
bound_element<Integer> be=new bound_element<>();
24+
belem=new bound_element<>();
25+
be.elem=new Integer(n+1);
26+
if(n>0)
27+
return e.elem;
28+
else
29+
return be.elem;
30+
}
31+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
generics.class
3+
--show-symbol-table
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^Type........: struct generics\$bound_element\<java::java.lang.Integer\> \{
7+
__CPROVER_string \@class_identifier; boolean \@lock; struct java.lang.Object \@java.lang.Object; struct java.lang.Integer \*elem; struct generics \*this\$0; \}$
8+
--

regression/cbmc-java/iterator2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
iterator2.class
3-
--cover location --unwind 3 --function iterator2.f
3+
--cover location --unwind 3 --function iterator2.f
44
^EXIT=0$
55
^SIGNAL=0$
66
^.*SATISFIED$

regression/cbmc/havoc_object1/main.c

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
int main()
2+
{
3+
int i=0;
4+
__CPROVER_havoc_object(&i);
5+
__CPROVER_assert(i==0, "i==0"); // should fail
6+
7+
int array[10];
8+
for(i=0; i<10; i++) array[i]=i;
9+
10+
__CPROVER_havoc_object(array);
11+
__CPROVER_assert(array[3]==3, "array[3]"); // should fail
12+
13+
struct { int i, j; } some_struct = { 1, 2 };
14+
__CPROVER_havoc_object(&some_struct.j);
15+
__CPROVER_assert(some_struct.i==1, "struct i"); // should fail
16+
__CPROVER_assert(some_struct.j==2, "struct j"); // should fail
17+
18+
// now conditional
19+
_Bool c;
20+
int *p=c?&i:&some_struct.i;
21+
i=20;
22+
some_struct.i=30;
23+
__CPROVER_havoc_object(p);
24+
if(c)
25+
{
26+
__CPROVER_assert(i==20, "i==20 (A)"); // should fail
27+
__CPROVER_assert(some_struct.i==30, "some_struct.i==30 (A)"); // should pass
28+
}
29+
else
30+
{
31+
__CPROVER_assert(i==20, "i==20 (B)"); // should pass
32+
__CPROVER_assert(some_struct.i==30, "some_struct.i==30 (B)"); // should fail
33+
}
34+
}
+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
^\*\* 6 of 8 failed.*$
8+
--

regression/cbmc/memset3/main.c

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <string.h>
2+
#include <stdlib.h>
3+
#include <assert.h>
4+
5+
int main()
6+
{
7+
int *A=malloc(sizeof(int)*4);
8+
9+
memset(A+20, 0, sizeof(int)); // out-of-bounds
10+
11+
return 0;
12+
}

0 commit comments

Comments
 (0)