Skip to content

Commit 0ef260a

Browse files
author
owen-jones-diffblue
authored
Merge pull request diffblue#374 from diffblue/CBMC_merge_2018-04-10
Cbmc merge 2018-04-10
2 parents 4d7a338 + 4183df5 commit 0ef260a

File tree

162 files changed

+2844
-1693
lines changed

Some content is hidden

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

162 files changed

+2844
-1693
lines changed

‎cbmc/regression/cbmc-java/lambda3/LambdaTest/Lamb1.class

164 Bytes
Binary file not shown.

‎cbmc/regression/cbmc-java/lambda3/LambdaTest/Test.class

1.41 KB
Binary file not shown.

‎cbmc/regression/cbmc-java/lambda3/LambdaTest/Test.java

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package LambdaTest;
2+
3+
interface Lamb1 {
4+
public Integer lambFunc1(Integer x);
5+
}
6+
7+
class Test {
8+
9+
public static Integer recvLambda(Integer y, Integer z) {
10+
Lamb1 lmb1 = (x) -> x = y + z; // Initializing in a lambda statement
11+
if (lmb1 != null && z != null) {
12+
return lmb1.lambFunc1(y);
13+
}
14+
return lmb1.lambFunc1(z);
15+
}
16+
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
LambdaTest/Test.class
3+
--show-symbol-table --function LambdaTest.Test.recvLambda
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
--
8+
This is to verify that parsing lambdas in a package does not crash.

‎cbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
FUTURE
1+
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property "java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1"
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎cbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
Test.class
33
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5 --verbosity 10
44
^EXIT=10$

‎cbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
FUTURE
1+
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property "java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1"
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎cbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
FUTURE
1+
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5 --verbosity 10
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎cbmc/regression/jbmc-strings/StringConcat/test_string_nondet.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
Test.class
33
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10
44
^EXIT=10$

‎cbmc/regression/jbmc-strings/StringEquals/Test.class

572 Bytes
Binary file not shown.

‎cbmc/regression/jbmc-strings/StringEquals/Test.java

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
// Uses CProverString, must be compiled with ../cprover/CProverString.java
2+
import org.cprover.*;
3+
14
public class Test {
25
public static void check(int i, String s) {
36
String t = "Hello World";
@@ -15,4 +18,49 @@ else if (i==4)
1518
else if (i==5)
1619
assert(s.equals(x));
1720
}
21+
22+
public static boolean referenceImplementation(String s, Object o) {
23+
if (! (o instanceof String))
24+
return false;
25+
26+
String s2 = (String) o;
27+
if (s.length() != s2.length())
28+
return false;
29+
30+
for (int i = 0; i < s.length(); i++) {
31+
if (CProverString.charAt(s, i) != CProverString.charAt(s2, i))
32+
return false;
33+
}
34+
35+
return true;
36+
}
37+
38+
public static boolean verifyNonNull(String s, Object o) {
39+
// Filter
40+
if (s == null || o == null)
41+
return false;
42+
43+
// Act
44+
boolean result = s.equals(o);
45+
boolean referenceResult = referenceImplementation(s, o);
46+
47+
// Assert
48+
assert result == referenceResult;
49+
50+
// Return
51+
return result;
52+
}
53+
54+
public static boolean verify(String s, Object o) {
55+
// Act
56+
boolean result = s.equals(o);
57+
boolean referenceResult = referenceImplementation(s, o);
58+
59+
// Assert
60+
assert result == referenceResult;
61+
62+
// Return
63+
return result;
64+
}
65+
1866
}

‎cbmc/regression/jbmc-strings/StringEquals/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ Test.class
33
--refine-strings --string-max-length 40 --function Test.check
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file Test.java line 6 .* SUCCESS
7-
assertion at file Test.java line 8 .* FAILURE
8-
assertion at file Test.java line 10 .* SUCCESS
9-
assertion at file Test.java line 12 .* FAILURE
10-
assertion at file Test.java line 14 .* SUCCESS
11-
assertion at file Test.java line 16 .* FAILURE
6+
assertion at file Test.java line 9 .* SUCCESS
7+
assertion at file Test.java line 11 .* FAILURE
8+
assertion at file Test.java line 13 .* SUCCESS
9+
assertion at file Test.java line 15 .* FAILURE
10+
assertion at file Test.java line 17 .* SUCCESS
11+
assertion at file Test.java line 19 .* FAILURE
1212
--

‎cbmc/regression/jbmc-strings/StringEquals/test_verify.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
Test.class
3+
--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 60 .* SUCCESS
7+
--
8+
--
9+
null case not handled currently
10+
TG-2179
11+

‎cbmc/regression/jbmc-strings/StringEquals/test_verify_non_null.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--refine-strings --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verifyNonNull
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 48 .* SUCCESS

‎cbmc/regression/jbmc-strings/StringIndexOf/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test.class
3-
--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null
3+
--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --string-max-length 100 --java-assume-inputs-non-null
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎cbmc/regression/jbmc-strings/literal-length/Test.class

623 Bytes
Binary file not shown.

‎cbmc/regression/jbmc-strings/literal-length/Test.java

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
public class Test {
2+
public static int check(int i) {
3+
String s = "\u0000";
4+
5+
if (i == 0)
6+
assert(s.length() == 1);
7+
else if (i == 1)
8+
assert(s.length() != 1);
9+
10+
return s.length();
11+
}
12+
}

‎cbmc/regression/jbmc-strings/literal-length/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
Test.class
3+
--refine-strings --function Test.check
4+
assertion at file Test.java line 6 .* SUCCESS
5+
assertion at file Test.java line 8 .* FAILURE
6+
^EXIT=10$
7+
^SIGNAL=0$

‎cbmc/regression/jbmc-strings/long_string/Test.class

985 Bytes
Binary file not shown.

‎cbmc/regression/jbmc-strings/long_string/Test.java

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
import org.cprover.CProverString;
2+
3+
public class Test {
4+
public static void check(String s, String t) {
5+
// Filter
6+
if(s == null || t == null)
7+
return;
8+
9+
// Act
10+
String u = s.concat(t);
11+
12+
// Filter out
13+
if(u.length() < 3_000_000)
14+
return;
15+
if(CProverString.charAt(u, 500_000) != 'a')
16+
return;
17+
if(CProverString.charAt(u, 2_000_000) != 'b')
18+
return;
19+
20+
// Assert
21+
assert(false);
22+
}
23+
24+
public static void checkAbort(String s, String t) {
25+
// Filter
26+
if(s == null || t == null)
27+
return;
28+
29+
// Act
30+
String u = s.concat(t);
31+
32+
// Filter out
33+
if(u.length() < 67_108_864)
34+
return;
35+
if(CProverString.charAt(u, 2_000_000) != 'b')
36+
return;
37+
38+
// Assert
39+
assert(false);
40+
}
41+
}

‎cbmc/regression/jbmc-strings/long_string/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
Test.class
3+
--refine-strings --function Test.check --string-max-input-length 2000000
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 21 .* FAILURE
7+
--
8+
--
9+
This checks that the solver manage to violate assertions even when this requires
10+
some very long strings, as long as they don't exceed the arbitrary limit that
11+
is set by the solver (64M characters).

‎cbmc/regression/jbmc-strings/long_string/test_abort.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--refine-strings --function Test.checkAbort
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
--
7+
--
8+
This tests should abort, because concretizing a string of the required
9+
length may take to much memory.

‎cbmc/src/cbmc/bmc.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -627,6 +627,8 @@ void bmct::setup_unwind()
627627
/// \param message: used for logging
628628
/// \param driver_configure_bmc: function provided by the driver program,
629629
/// which applies driver-specific configuration to a bmct before running.
630+
/// \param callback_after_symex: optional callback to be run after symex.
631+
/// See class member `bmct::driver_callback_after_symex` for details.
630632
int bmct::do_language_agnostic_bmc(
631633
const optionst &opts,
632634
abstract_goto_modelt &model,

‎cbmc/src/common

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
2727
# Linux-ish
2828
LIBEXT = .a
2929
OBJEXT = .o
30+
DEPEXT = .d
3031
ifeq ($(BUILD_ENV_),MinGW)
3132
EXEEXT = .exe
3233
else
@@ -99,6 +100,7 @@ else ifeq ($(BUILD_ENV_),Cygwin)
99100
# use these for Cygwin:
100101
LIBEXT = .a
101102
OBJEXT = .o
103+
DEPEXT = .d
102104
EXEEXT = .exe
103105
CFLAGS ?= -Wall -O2
104106
CXXFLAGS ?= -Wall -O2
@@ -131,6 +133,7 @@ else ifeq ($(BUILD_ENV_),MSVC)
131133
# use these for Visual Studio:
132134
LIBEXT = .lib
133135
OBJEXT = .obj
136+
DEPEXT = .dep
134137
EXEEXT = .exe
135138
CFLAGS ?= /W3 /O2 /GF
136139
CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF
@@ -159,18 +162,14 @@ else
159162
endif
160163

161164
# select default solver to be minisat2 if no other is specified
162-
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
165+
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT),)
163166
MINISAT2 = ../../minisat-2.2.1
164167
endif
165168

166169
ifneq ($(IPASIR),)
167170
CP_CXXFLAGS += -DHAVE_IPASIR
168171
endif
169172

170-
ifneq ($(PRECOSAT),)
171-
CP_CXXFLAGS += -DHAVE_PRECOSAT
172-
endif
173-
174173
ifneq ($(PICOSAT),)
175174
CP_CXXFLAGS += -DHAVE_PICOSAT
176175
endif
@@ -213,7 +212,7 @@ CP_CXXFLAGS += $(CXXFLAGS) $(INCLUDES)
213212
OBJ += $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC)))
214213
OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
215214

216-
.SUFFIXES: .cc .d .cpp
215+
.SUFFIXES: .cc $(DEPEXT) .cpp
217216

218217
%.o:%.cpp
219218
$(CXX) -c $(CP_CXXFLAGS) -o $@ $<
@@ -236,9 +235,9 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
236235

237236
clean:
238237
$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
239-
$(patsubst %.cpp, %.d, $(filter %.cpp, $(SRC))) \
238+
$(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \
240239
$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
241-
$(patsubst %.cc, %.d, $(filter %.cc, $(SRC))) \
240+
$(patsubst %.cc, %$(DEPEXT), $(filter %.cc, $(SRC))) \
242241
$(CLEANFILES)
243242

244243
.PHONY: first_target clean all
@@ -255,7 +254,7 @@ sources: Makefile
255254
# include .depend
256255
# endif
257256

258-
D_FILES1 = $(SRC:.c=.d)
259-
D_FILES = $(D_FILES1:.cpp=.d)
257+
D_FILES1 = $(SRC:.c=$(DEPEXT))
258+
D_FILES = $(D_FILES1:.cpp=$(DEPEXT))
260259

261260
-include $(D_FILES)

‎cbmc/src/config.inc

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ endif
2424
#LIB_GLPK = -lglpk
2525

2626
# SAT-solvers we have
27-
#PRECOSAT = ../../precosat-576-7e5e66f-120112
2827
#PICOSAT = ../../picosat-959
2928
#LINGELING = ../../lingeling-587f-4882048-110513
3029
#CHAFF = ../../zChaff
@@ -33,16 +32,11 @@ endif
3332
#MINISAT2 = ../../minisat-2.2.1
3433
#IPASIR = ../../ipasir
3534
#GLUCOSE = ../../glucose-syrup
36-
#SMVSAT =
3735

3836
# Extra library for SAT solver. This should link to the archive file to be used
3937
# when linking against an IPASIR solver.
4038
LIBSOLVER =
4139

42-
ifneq ($(PRECOSAT),)
43-
CP_CXXFLAGS += -DSATCHECK_PRECOSAT
44-
endif
45-
4640
ifneq ($(PICOSAT),)
4741
CP_CXXFLAGS += -DSATCHECK_PICOSAT
4842
endif
@@ -71,10 +65,6 @@ ifneq ($(GLUCOSE),)
7165
CP_CXXFLAGS += -DSATCHECK_GLUCOSE
7266
endif
7367

74-
ifneq ($(SMVSAT),)
75-
CP_CXXFLAGS += -DSATCHECK_SMVSAT
76-
endif
77-
7868
# Signing identity for MacOS Gatekeeper
7969

8070
OSX_IDENTITY="Developer ID Application: Daniel Kroening"

‎cbmc/src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -588,8 +588,6 @@ void cpp_typecheck_resolvet::make_constructors(
588588
{
589589
resolve_identifierst new_identifiers;
590590

591-
resolve_identifierst::iterator next;
592-
593591
for(resolve_identifierst::iterator
594592
it=identifiers.begin();
595593
it!=identifiers.end();

‎cbmc/src/goto-instrument/cover_basic_blocks.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ class message_handlert;
2121
class cover_blocks_baset
2222
{
2323
public:
24+
virtual ~cover_blocks_baset() = default;
2425
/// \param t a goto instruction
2526
/// \return the block number of the block
2627
/// the given goto instruction is part of

‎cbmc/src/goto-instrument/cover_instrument.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ class goal_filterst;
2525
class cover_instrumenter_baset
2626
{
2727
public:
28+
virtual ~cover_instrumenter_baset() = default;
2829
cover_instrumenter_baset(
2930
const symbol_tablet &_symbol_table,
3031
const goal_filterst &_goal_filters,

0 commit comments

Comments
 (0)