Skip to content

Commit 199e814

Browse files
author
Owen Jones
committed
Squashed 'cbmc/' changes from 6a10f1a..5d3ea03
5d3ea03 Merge pull request diffblue#2693 from zhixing-xu/fix_rw_range_upper 2b40338 Update test.desc c6d0427 Merge pull request diffblue#2674 from diffblue/msvc-link 318474f Merge pull request diffblue#2678 from romainbrenguier/feature/extend-builtin-functions-part3 c63030f Regression test for goto-link personality 64fedd0 Microsoft LINK personality d9f9dd9 Merge pull request diffblue#2688 from tautschnig/concat-dir-file 99946fc Merge pull request diffblue#2675 from diffblue/goto-cl-echo-file 252d857 Merge pull request diffblue#2687 from tautschnig/fo-directory 0d7ebd5 Fixed a problem where the rw_set range's upper bound not set correctly 29eab32 goto-cl: Fail invocation of trying to compile multiple files to non-directory 7f587c4 Fix concat_dir_file for Windows and unit-test it a44468b Document string_builtin_function::eval ecc0e43 Document eval_is_upper_case a345d30 Document eval_string 58307a0 Tests for String.toUpperCase 71de2e3 Tests for String.toLowerCase 579d00c Remove redundant function application ID check e2961b5 Add builtin class for string_to_upper_case fe9071b Make to_upper_case work for Latin-1 supplement 53ccd3f Refactor string_to_upper_case be477c9 Remove assumptions that input char are < 0x100 836cbad Extract an is_upper_case function 1137ffd Improve documentation of add_axioms_for_to_lower_case a71f2c0 Implement builtin string_to_lower_case function fae6a48 Merge pull request diffblue#2467 from tautschnig/vs-except 24de513 Merge pull request diffblue#2474 from tautschnig/vs-identifier e14f2f2 Merge pull request diffblue#2685 from diffblue/clcache-again 08698cc Merge pull request diffblue#2681 from diffblue/remove-aig d42020b remove --aig option cd4a163 AWS codebuild windows: set clcache base directory 1ba928c cleanup unnecessary path from configuration file 8c4801b Refactor add_axioms_for_to_lower_case 4291232 Merge pull request diffblue#2686 from diffblue/buildspec-apt-cache 3adb717 AWS codebuild: cache apt lists and packages 0efb169 remove AIGs 3a9c825 Merge pull request diffblue#2682 from diffblue/fix-clcache b9b5660 Merge pull request diffblue#2483 from tautschnig/vs-java-parameters a66ab1e CL prints the name of the file that's compiled onto stdout 0698a5f Merge pull request diffblue#2673 from diffblue/goto-cl-Fo 75855bf Java front-end: remove unused parameters 4df2187 debugging output to resolve seg fault 5bc7456 goto-cl: /Fo can set an output directory a43e4fa add is_directory to file_util.h 4ad91fb Codebuild for windows: set up cache path properly effb01b Merge pull request diffblue#2641 from diffblue/typedef-type 5ef2802 Merge pull request diffblue#2679 from tautschnig/version-string 2efea52 Refine test patterns to avoid spurious matches aa7ebbc Merge pull request diffblue#2672 from diffblue/goto-cc-multiple-source-files aaea781 Merge pull request diffblue#2671 from diffblue/fix_get_base_name 8b51faf fix get_base_name 694daaf gcc mode: error in case multiple files are given with -c and -o 09fdca3 Merge pull request diffblue#2643 from svorenova/fixup-nondet-static d42054a Merge pull request diffblue#2669 from diffblue/spurious-cover-test b391c9e introduce typedef_type in the C frontend 114030b Merge pull request diffblue#2664 from romainbrenguier/feature/extend-builtin-functions-part2 46f6231 cbmc test no longer uses --cover daff1d1 Make nondet-static replace lines in CPROVER_init 1bca129 Merge pull request diffblue#2665 from tautschnig/gcc-conditional-stmt 31366ad Tests for StringBuilder.setCharAt f4285e7 Add builtin support for string_set_char 2a8ea0f Better specify out-of-bounds case for set_char 9415a24 Refactor add_axioms_for_set_char 9762886 Refactor string_concat_char builtin function b62bf01 Make nondet-static check for ID_C_no_nondet_initialization a50562e Mark java.lang.String.Literals with ID_C_constant b3c08d3 Mark internal Java variables with ID_C_no_nondet_initialization f2dc978 Add a new comment to mark variables that should not be nondet initialized da7966c Merge pull request diffblue#2645 from mmuesly/feature_test_posix_memalign cb4a340 Merge pull request diffblue#2647 from diffblue/cleanout-jar-filet 2b27a2d Merge pull request diffblue#2622 from martin-cs/feature/context-sensitive-ait-merge-2 00b26a8 Adds a test for posix_memalign in stdlib.c 0f5a057 Merge pull request diffblue#2667 from tautschnig/slicer-cleanup 16e6462 Remove no-longer-used ifdef 96d345b Clean GCC conditional expressions in right-hand sides of declarations 086c266 Merge pull request diffblue#2651 from smowton/smowton/feature/unroll-enum-clone-loops f69b244 Merge pull request diffblue#2625 from smowton/smowton/feature/value-set-accuracy 730b3e2 Merge pull request diffblue#2655 from romainbrenguier/feature/extend-builtin-functions c4569dd remove java_class_loader_limitt from jar_filet e0f954d Merge pull request diffblue#2659 from smowton/smowton/fix/cmake-third-time-is-charm 7f547b1 Merge pull request diffblue#2656 from smowton/smowton/fix/testsuite-name 3a1593b Tests for String.valueOf(int) 7414d76 Add builtin support for string_of_int 0b44c89 Add version of make_string accepting iterators f81f082 Rename function to add_axioms_for_string_of_int 9a2a7c2 Switch version.cpp from a rule product to a byproduct 943d60c Value set: handle with, array and struct expressions more accurately 4f158a3 Mark regression tests as expecting failure for symex driven loading c9a53f9 Add regression tests for changes to JBMC enumeration support a985eae Interpreter: deal with member-of-constant-struct expressions 361469b Change source location of jump target in {table|lookup}switch 6270968 java-unwind-enum-static: also unwind clone loop in Enum.values() 714de0d Symex: expose call stack to unwinding decision making fb239ef Fix jbmc-generic-symex-driven-lazy-loading test name 28ba192 Strengthen the invariant on what are acceptable function calls. 773bc86 Convert various comments, asserts and throws into invariants. e65f027 Add comments to the abstract interpreter interface. 1fe0796 Convert various older domains to use the more recent ait API. afe32b7 Refactor the methods that access "the abstract domain at a location". aa743b3 Remove unused exception name from catch statement 5703504 Remove unused parameter identifier git-subtree-dir: cbmc git-subtree-split: 5d3ea03
1 parent e7ed234 commit 199e814

File tree

154 files changed

+2711
-1682
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

+2711
-1682
lines changed

‎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\**\*'

‎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/**/*'

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

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

1.49 KB
Binary file not shown.

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

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

‎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

‎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

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

1.67 KB
Binary file not shown.

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

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

‎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

‎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

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

1.7 KB
Binary file not shown.

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

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

‎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

‎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

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

1.6 KB
Binary file not shown.

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