Skip to content

Commit c4766c9

Browse files
author
owen-jones-diffblue
authored
Merge pull request diffblue#537 from diffblue/CBMC_merge_2018-08-08
SEC-599: Cbmc merge 2018-08-08
2 parents 236b98a + 718b63c commit c4766c9

File tree

154 files changed

+2713
-1684
lines changed

Some content is hidden

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

154 files changed

+2713
-1684
lines changed

‎cbmc/buildspec-windows.yml

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,24 +11,27 @@ phases:
1111
commands:
1212
- |
1313
$env:Path = "C:\tools\cygwin\bin;$env:Path"
14-
C:\tools\cygwin\bin\bash -c "make -C src minisat2-download DOWNLOADER=wget"
14+
bash -c "make -C src minisat2-download DOWNLOADER=wget"
1515
1616
- |
1717
$env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path"
1818
$env:CLCACHE_DIR = "C:\clcache"
19+
$env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName
1920
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C src BUILD_ENV=MSVC" '
2021
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C unit all BUILD_ENV=MSVC" '
2122
2223
- |
2324
$env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path"
2425
$env:CLCACHE_DIR = "C:\clcache"
26+
$env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName
2527
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src setup-submodules" && bash -c "make CXX=clcache.exe -j4 -C jbmc/src BUILD_ENV=MSVC" '
2628
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C jbmc/unit all BUILD_ENV=MSVC" '
2729
2830
- |
2931
# display cache stats
3032
$env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path"
3133
$env:CLCACHE_DIR = "C:\clcache"
34+
$env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName
3235
cmd /c 'clcache -s'
3336
3437
post_build:
@@ -63,6 +66,7 @@ phases:
6366
- |
6467
$env:Path = "C:\tools\cygwin\bin;$env:Path"
6568
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
69+
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/goto-cl test BUILD_ENV=MSVC" '
6670
6771
- |
6872
$env:Path = "C:\tools\cygwin\bin;$env:Path"
@@ -81,4 +85,4 @@ artifacts:
8185

8286
cache:
8387
paths:
84-
- 'c:\clcache'
88+
- 'c:\clcache\**\*'

‎cbmc/buildspec.yml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,4 +31,6 @@ artifacts:
3131
files:
3232
cache:
3333
paths:
34+
- '/var/cache/apt/**/*'
35+
- '/var/lib/apt/lists/**/*'
3436
- '/root/.ccache/**/*'

‎cbmc/jbmc/regression/jbmc-generics/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ add_test_pl_tests(
33
)
44

55
add_test_pl_profile(
6-
"jbmc-symex-driven-lazy-loading"
6+
"jbmc-generics-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"

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

1.49 KB
Binary file not shown.

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
public class Test {
2+
public String det()
3+
{
4+
StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
5+
builder.setCharAt(3, '!');
6+
builder.setCharAt(5, '!');
7+
builder.setCharAt(7, '!');
8+
builder.setCharAt(9, '!');
9+
builder.setCharAt(13, '!');
10+
builder.setCharAt(15, '!');
11+
builder.setCharAt(17, '!');
12+
builder.setCharAt(19, '!');
13+
builder.setCharAt(4, ':');
14+
builder.setCharAt(5, ':');
15+
builder.setCharAt(6, ':');
16+
builder.setCharAt(9, ':');
17+
builder.setCharAt(10, ':');
18+
builder.setCharAt(11, ':');
19+
builder.setCharAt(16, ':');
20+
builder.setCharAt(18, ':');
21+
return builder.toString();
22+
}
23+
24+
public String nonDet(String s, char c, int i)
25+
{
26+
StringBuilder builder = new StringBuilder(s);
27+
if(i + 5 >= s.length() || 19 >= s.length() || i < 0)
28+
return "Out of bounds";
29+
builder.setCharAt(i, c);
30+
builder.setCharAt(i+5, 'x');
31+
builder.setCharAt(7, '!');
32+
builder.setCharAt(9, '!');
33+
builder.setCharAt(13, '!');
34+
builder.setCharAt(15, '!');
35+
builder.setCharAt(17, '!');
36+
builder.setCharAt(19, '!');
37+
builder.setCharAt(4, ':');
38+
builder.setCharAt(5, ':');
39+
builder.setCharAt(6, c);
40+
builder.setCharAt(9, ':');
41+
builder.setCharAt(10, ':');
42+
builder.setCharAt(11, ':');
43+
builder.setCharAt(16, ':');
44+
builder.setCharAt(18, ':');
45+
return builder.toString();
46+
}
47+
48+
public String withDependency(boolean b)
49+
{
50+
StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
51+
builder.setCharAt(3, '!');
52+
builder.setCharAt(5, '!');
53+
54+
if(b) {
55+
assert builder.toString().startsWith("abc!");
56+
} else {
57+
assert !builder.toString().startsWith("abc!");
58+
}
59+
return builder.toString();
60+
}
61+
62+
}

‎cbmc/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
Test.class
3+
--function Test.withDependency --max-nondet-string-length 1000
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 55 .*: SUCCESS
7+
assertion at file Test.java line 57 .*: FAILURE
8+
--
9+
--
10+
Check that when a dependency is present, the correct constraints are added
11+
12+

‎cbmc/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.det --verbosity 10 --cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 21 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

‎cbmc/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 45 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

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

1.67 KB
Binary file not shown.

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

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
public class Test {
2+
public String det()
3+
{
4+
StringBuilder builder = new StringBuilder();
5+
builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase());
6+
builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toLowerCase());
7+
builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toLowerCase());
8+
builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toLowerCase());
9+
builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toLowerCase());
10+
return builder.toString();
11+
}
12+
13+
public String nonDet(String s)
14+
{
15+
if(s.length() < 20)
16+
return "Short string";
17+
if(!s.startsWith("A"))
18+
return "String not starting with A";
19+
20+
StringBuilder builder = new StringBuilder();
21+
builder.append(s.toLowerCase());
22+
builder.append(s.toLowerCase());
23+
builder.append(":");
24+
builder.append(s);
25+
builder.append(":");
26+
builder.append(s.toLowerCase());
27+
builder.append(s.toLowerCase());
28+
return builder.toString();
29+
}
30+
31+
public String withDependency(String s, boolean b)
32+
{
33+
// Filter
34+
if(s == null || s.length() < 20)
35+
return "Short string";
36+
if(!s.endsWith("A"))
37+
return "String not ending with A";
38+
39+
// Act
40+
String result = s + s.toLowerCase();
41+
42+
// Assert
43+
if(b) {
44+
assert(result.endsWith("a"));
45+
} else {
46+
assert(!result.endsWith("a"));
47+
}
48+
return result;
49+
}
50+
}

‎cbmc/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 44 .*: SUCCESS
7+
assertion at file Test.java line 46 .*: FAILURE
8+
--
9+
--
10+
Check that when there are dependencies, axioms are adde correctly.

‎cbmc/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.det --verbosity 10 --cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 9 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

‎cbmc/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 27 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

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

1.7 KB
Binary file not shown.

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

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
public class Test {
2+
public String det()
3+
{
4+
StringBuilder builder = new StringBuilder();
5+
builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase());
6+
builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toUpperCase());
7+
builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase());
8+
builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase());
9+
builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase());
10+
return builder.toString();
11+
}
12+
13+
public String nonDet(String s)
14+
{
15+
if(s.length() < 20)
16+
return "Short string";
17+
if(!s.startsWith("a"))
18+
return "String not starting with a";
19+
20+
StringBuilder builder = new StringBuilder();
21+
builder.append(s.toUpperCase());
22+
builder.append(s.toUpperCase());
23+
builder.append(":");
24+
builder.append(s);
25+
builder.append(":");
26+
builder.append(s.toUpperCase());
27+
builder.append(s.toUpperCase());
28+
return builder.toString();
29+
}
30+
31+
public String withDependency(String s, boolean b)
32+
{
33+
// Filter
34+
if(s == null || s.length() < 20)
35+
return "Short string";
36+
if(!s.endsWith("a"))
37+
return "String not ending with a";
38+
39+
// Act
40+
String result = s + s.toUpperCase();
41+
42+
// Assert
43+
if(b) {
44+
assert(result.endsWith("A"));
45+
} else {
46+
assert(!result.endsWith("A"));
47+
}
48+
return result;
49+
}
50+
}

‎cbmc/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 44 .*: SUCCESS
7+
assertion at file Test.java line 46 .*: FAILURE
8+
--
9+
--
10+
Check that when there are dependencies, axioms are added correctly.

‎cbmc/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.det --verbosity 10 --cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 9 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

‎cbmc/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 27 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

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

1.6 KB
Binary file not shown.

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

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
public class Test
2+
{
3+
public static String checkDet()
4+
{
5+
String tmp = String.valueOf(1000000);
6+
tmp = String.valueOf(1000001);
7+
tmp = String.valueOf(1000002);
8+
tmp = String.valueOf(1000003);
9+
tmp = String.valueOf(1000004);
10+
tmp = String.valueOf(1000005);
11+
tmp = String.valueOf(-1000001);
12+
tmp = String.valueOf(-1000002);
13+
tmp = String.valueOf(-1000003);
14+
tmp = String.valueOf(1000004);
15+
tmp = String.valueOf(1000005);
16+
tmp = String.valueOf(-1000001);
17+
tmp = String.valueOf(-1000002);
18+
tmp = String.valueOf(1000003);
19+
tmp = String.valueOf(1000004);
20+
tmp = String.valueOf(1000005);
21+
tmp = String.valueOf(1000001);
22+
tmp = String.valueOf(-1000002);
23+
tmp = String.valueOf(-1000003);
24+
tmp = String.valueOf(1000004);
25+
tmp = String.valueOf(1000005);
26+
return tmp;
27+
}
28+
29+
public static String checkNonDet(int i)
30+
{
31+
String tmp = String.valueOf(1000000);
32+
tmp = String.valueOf(i + 1);
33+
tmp = String.valueOf(i + 2);
34+
tmp = String.valueOf(i + 3);
35+
tmp = String.valueOf(i + 4);
36+
tmp = String.valueOf(i + 5);
37+
tmp = String.valueOf(i - 1);
38+
tmp = String.valueOf(i - 2);
39+
tmp = String.valueOf(i - 3);
40+
tmp = String.valueOf(i - 4);
41+
tmp = String.valueOf(i - 5);
42+
tmp += " ";
43+
tmp += String.valueOf(i);
44+
tmp += " ";
45+
tmp += String.valueOf(i + 2);
46+
tmp += " ";
47+
tmp += String.valueOf(i + 3);
48+
tmp += " ";
49+
tmp += String.valueOf(-i);
50+
tmp += " ";
51+
tmp += String.valueOf(-i + 1);
52+
tmp += " ";
53+
tmp += String.valueOf(-i - 2);
54+
return tmp;
55+
}
56+
57+
public static void checkWithDependency(boolean b)
58+
{
59+
String s = String.valueOf(12);
60+
if (b) {
61+
assert(s.startsWith("12"));
62+
}
63+
else {
64+
assert(!s.startsWith("12"));
65+
}
66+
}
67+
68+
}

0 commit comments

Comments
 (0)