Skip to content

Commit 4f45985

Browse files
smowtonsmowton
authored
Merge pull request diffblue#271 from diffblue/smowton/merge_develop_2017_11_16
Merge latest cbmc-develop
2 parents 7619d15 + 471180d commit 4f45985

File tree

365 files changed

+9277
-3852
lines changed

Some content is hidden

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

365 files changed

+9277
-3852
lines changed

‎CMakeLists.txt

+46
Original file line numberDiff line numberDiff line change
@@ -44,3 +44,49 @@ if(${enable_cbmc_tests})
4444
endif()
4545
add_subdirectory(unit)
4646
add_subdirectory(regression)
47+
48+
set_target_properties(
49+
analyses
50+
ansi-c
51+
assembler
52+
big-int
53+
cbmc
54+
cbmc-lib
55+
clobber
56+
clobber-lib
57+
cpp
58+
driver
59+
goto-analyzer
60+
goto-analyzer-lib
61+
goto-cc
62+
goto-cc-lib
63+
goto-diff
64+
goto-diff-lib
65+
goto-instrument
66+
goto-instrument-lib
67+
goto-programs
68+
goto-symex
69+
java_bytecode
70+
jbmc
71+
jbmc-lib
72+
jsil
73+
json
74+
langapi
75+
linking
76+
miniBDD
77+
miniz
78+
mmcc
79+
pointer-analysis
80+
solvers
81+
string_utils
82+
test-bigint
83+
testing-utils
84+
unit
85+
util
86+
xml
87+
88+
PROPERTIES
89+
CXX_STANDARD 11
90+
CXX_STANDARD_REQUIRED true
91+
XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
92+
)

‎CODEOWNERS

+41-20
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,57 @@
11
# These owners will be the default owners for everything in the repo.
2-
* @kroening @tautschnig @peterschrammel
2+
* @kroening @tautschnig @peterschrammel @smowton @chrisr-diffblue
33

4-
src/java_bytecode/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
5-
src/jbmc/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
6-
src/miniz/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli
4+
# These files should rarely change
75

8-
src/ansi-c/ @marek-trtik @kroening @tautschnig
6+
src/big-int/ @kroening
7+
src/ansi-c/ @kroening @tautschnig
8+
src/assembler/ @kroening @tautschnig
9+
src/goto-cc/ @kroening @tautschnig
10+
src/linking/ @kroening @tautschnig
11+
src/memory-models/ @kroening @tautschnig
12+
src/goto-symex/ @kroening @tautschnig @peterschrammel
13+
src/json/ @kroening @tautschnig @peterschrammel
14+
src/langapi/ @kroening @tautschnig @peterschrammel
15+
src/xmllang/ @kroening @tautschnig @peterschrammel
16+
src/nonstd/ @smowton @peterschrammel
17+
src/solvers/cvc @martin-cs @kroening
18+
src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
19+
src/solvers/floatbv @martin-cs @kroening
20+
src/solvers/miniBDD @tautschnig @kroening
21+
src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
22+
src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
23+
src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
24+
src/miniz/ @smowton @mgudemann @peterschrammel
925

10-
src/cpp/ @marek-trtik @kroening @tautschnig
1126

12-
CMakeLists.txt @reuk @thk123
27+
# These files change frequently and changes are high-risk
1328

14-
cmake/ @reuk @thk123
29+
src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
30+
src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
31+
src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
32+
src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
33+
src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
34+
src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
35+
src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
1536

16-
src/solvers/ @martin-cs @romainbrenguier @antlechner @kroening
1737

18-
src/analyses/ @martin-cs @peterschrammel @thk123 @marek-trtik @NathanJPhillips
38+
# These files change frequently and changes are medium-risk
1939

20-
src/pointer-analysis/ @martin-cs @peterschrammel @thk123 @marek-trtik
40+
src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
41+
src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
42+
src/goto-diff/ @tautschnig @peterschrammel
43+
src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
44+
src/cpp/ @kroening @tautschnig @peterschrammel
2145

22-
src/goto-analyzer/ @martin-cs @peterschrammel @thk123 @marek-trtik
2346

24-
src/goto-instrument/ @martin-cs @peterschrammel @thk123 @marek-trtik
25-
26-
src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik
27-
28-
src/linking/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik
47+
# These files change frequently and changes are low-risk
2948

3049
unit/ @diffblue/cbmc-developers
31-
3250
regression/ @diffblue/cbmc-developers
3351

34-
.travis.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
35-
appveyor.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
52+
CMakeLists.txt @reuk @chrisr-diffblue
53+
cmake/ @reuk @chrisr-diffblue
3654

55+
scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
56+
.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
57+
appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel

‎appveyor.yml

+1
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,7 @@ test_script:
8383
rmdir /s /q cbmc\byte_update7
8484
rmdir /s /q cbmc\pipe1
8585
rmdir /s /q cbmc\unsigned___int128
86+
rmdir /s /q cbmc-cpp
8687
rmdir /s /q cpp\Decltype1
8788
rmdir /s /q cpp\Decltype2
8889
rmdir /s /q cpp\Function_Overloading1

‎regression/CMakeLists.txt

+7-4
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,9 @@
1-
set(CMAKE_CXX_STANDARD 11)
2-
set(CMAKE_CXX_STANDARD_REQUIRED true)
3-
41
set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
52

63
macro(add_test_pl_profile name cmdline flag profile)
74
add_test(
85
NAME "${name}-${profile}"
9-
COMMAND ${test_pl_path} -c ${cmdline} ${flag}
6+
COMMAND ${test_pl_path} -p -c ${cmdline} ${flag}
107
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
118
)
129
set_tests_properties("${name}-${profile}" PROPERTIES
@@ -25,15 +22,21 @@ endmacro(add_test_pl_tests)
2522

2623
add_subdirectory(ansi-c)
2724
add_subdirectory(cbmc)
25+
add_subdirectory(cbmc-cover)
26+
add_subdirectory(cbmc-cpp)
2827
add_subdirectory(cbmc-java)
2928
add_subdirectory(cbmc-java-inheritance)
3029
add_subdirectory(cpp)
3130
add_subdirectory(goto-analyzer)
31+
add_subdirectory(goto-analyzer-taint)
3232
add_subdirectory(goto-cc-cbmc)
3333
add_subdirectory(goto-cc-goto-analyzer)
3434
add_subdirectory(goto-diff)
3535
add_subdirectory(goto-instrument)
3636
add_subdirectory(goto-instrument-typedef)
37+
if(NOT WIN32)
38+
add_subdirectory(goto-gcc)
39+
endif()
3740
add_subdirectory(invariants)
3841
add_subdirectory(jbmc-strings)
3942
add_subdirectory(strings)

‎regression/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
DIRS = ansi-c \
22
cbmc \
33
cbmc-cover \
4+
cbmc-cpp \
45
cbmc-java \
56
cbmc-java-inheritance \
67
cpp \

‎regression/ansi-c/Makefile

+2-8
Original file line numberDiff line numberDiff line change
@@ -10,16 +10,10 @@ else
1010
endif
1111

1212
test:
13-
@if ! ../test.pl -c $(exe) ; then \
14-
../failed-tests-printer.pl ; \
15-
exit 1 ; \
16-
fi
13+
@../test.pl -p -c $(exe)
1714

1815
tests.log: ../test.pl
19-
@if ! ../test.pl -c $(exe) ; then \
20-
../failed-tests-printer.pl ; \
21-
exit 1 ; \
22-
fi
16+
@../test.pl -p -c $(exe)
2317

2418
show:
2519
@for dir in *; do \

‎regression/cbmc-cover/CMakeLists.txt

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"$<TARGET_FILE:cbmc>"
3+
)

‎regression/cbmc-cover/Makefile

+2-8
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,10 @@
11
default: tests.log
22

33
test:
4-
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
5-
../failed-tests-printer.pl ; \
6-
exit 1 ; \
7-
fi
4+
@../test.pl -p -c ../../../src/cbmc/cbmc
85

96
tests.log: ../test.pl
10-
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
11-
../failed-tests-printer.pl ; \
12-
exit 1 ; \
13-
fi
7+
@../test.pl -p -c ../../../src/cbmc/cbmc
148

159
show:
1610
@for dir in *; do \

‎regression/cbmc-cpp/CMakeLists.txt

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"$<TARGET_FILE:cbmc>"
3+
)

‎regression/cbmc-cpp/FunctionParam1/main.cpp

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
int x;
3+
4+
void g(int i){
5+
x=i;
6+
}
7+
8+
int main() {
9+
g(3);
10+
assert(x==3);
11+
}
12+

‎regression/cbmc-cpp/FunctionParam1/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.cpp
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-cpp/MethodParam1/main.cpp

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
unsigned x;
3+
4+
class ct {
5+
void f(int i) {
6+
x=x+i;
7+
}
8+
};
9+
10+
int main() {
11+
unsigned r;
12+
x=r%3;
13+
ct c;
14+
c.f(2);
15+
assert(x<4);
16+
assert(x<5);
17+
}
18+

‎regression/cbmc-cpp/MethodParam1/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.cpp
3+
4+
instance is SATISFIABLE$
5+
instance is UNSATISFIABLE$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
^VERIFICATION FAILED$
9+
--
10+
^warning: ignoring

‎regression/cbmc-cpp/union2/main.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <assert.h>
12
struct A
23
{
34
union

‎regression/cbmc-java-inheritance/Makefile

+2-8
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,10 @@
11
default: tests.log
22

33
test:
4-
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
5-
../failed-tests-printer.pl ; \
6-
exit 1 ; \
7-
fi
4+
@../test.pl -p -c ../../../src/jbmc/jbmc
85

96
tests.log: ../test.pl
10-
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
11-
../failed-tests-printer.pl ; \
12-
exit 1 ; \
13-
fi
7+
@../test.pl -p -c ../../../src/jbmc/jbmc
148

159
show:
1610
@for dir in *; do \

‎regression/cbmc-java/Makefile

+2-8
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,10 @@
11
default: tests.log
22

33
test:
4-
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
5-
../failed-tests-printer.pl ; \
6-
exit 1 ; \
7-
fi
4+
@../test.pl -p -c ../../../src/jbmc/jbmc
85

96
tests.log: ../test.pl
10-
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
11-
../failed-tests-printer.pl ; \
12-
exit 1 ; \
13-
fi
7+
@../test.pl -p -c ../../../src/jbmc/jbmc
148

159
show:
1610
@for dir in *; do \

‎regression/cbmc-java/classpath2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
jarfile3.class
3-
--function jarfile3.f --java-cp-include-files "jarfile3\.class"
3+
--function jarfile3.f --java-cp-include-files 'jarfile3\.class'
44
^EXIT=10$
55
^SIGNAL=0$
66
.*SUCCESS$

‎regression/cbmc-java/divide_by_zero/DivideByZero.class

284 Bytes
Binary file not shown.

‎regression/cbmc-java/divide_by_zero/DivideByZero.java

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
public class DivideByZero {
2+
public static void main(String args[]) {
3+
int i=0;
4+
int j=10/i;
5+
}
6+
}

‎regression/cbmc-java/divide_by_zero/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
DivideByZero.class
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
Denominator should be nonzero: FAILURE
7+
^VERIFICATION FAILED
8+
--
9+
^warning: ignoring

‎regression/cbmc-java/function1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Main.class
3-
--function "Other.fail:()V"
3+
--function 'Other.fail:()V'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎regression/cbmc-java/function2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Main.class
3-
--function "D.fail:()V"
3+
--function 'D.fail:()V'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎regression/cbmc-java/function3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
Main.class
3-
--function "A.dummy:()V"
3+
--function 'A.dummy:()V'
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc-java/function4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
Main.class
3-
--function "Other.fail"
3+
--function 'Other.fail'
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc-java/generic_class_bound1/A.class

84 Bytes
Binary file not shown.

‎regression/cbmc-java/generic_class_bound1/B.class

84 Bytes
Binary file not shown.

‎regression/cbmc-java/generic_class_bound1/C.class

84 Bytes
Binary file not shown.

‎regression/cbmc-java/generic_class_bound1/Gn.class

831 Bytes
Binary file not shown.

‎regression/cbmc-java/generic_class_bound1/Gn.java

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
interface A{}
2+
interface B{}
3+
interface C{}
4+
interface L<T> extends A,B,C{}
5+
6+
public class Gn<T extends L<? extends B>>{
7+
Gn<?> ex1;
8+
public void foo1(Gn<?> ex1){
9+
if(ex1 != null)
10+
this.ex1 = ex1;
11+
}
12+
public static void main(String[] args) {
13+
System.out.println("ddfsdf");
14+
}
15+
}

‎regression/cbmc-java/generic_class_bound1/L.class

183 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)