Skip to content

Commit c99cba2

Browse files
smowtonsmowton
committed
Squashed 'cbmc/' changes from 9441a92..e6d196d
e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d
1 parent 43bd605 commit c99cba2

File tree

95 files changed

+2005
-2914
lines changed

Some content is hidden

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

95 files changed

+2005
-2914
lines changed

‎jbmc/regression/jbmc-strings/max-length/test1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
44
^EXIT=0$
55
^SIGNAL=0$
6-
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS
6+
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS

‎jbmc/regression/jbmc-strings/max-length/test2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE
6+
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE

‎jbmc/regression/jbmc-strings/max-length/test3.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE
6+
assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE

‎jbmc/regression/jbmc/ClassCastException2/A.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ClassCastException2/B.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ClassCastException2/C.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ClassCastException2/ClassCastExceptionTest.class

-251 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/JumpSimplification/Test.class

299 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/JumpSimplification/Test.java

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class Test {
2+
3+
public int foo(int i) {
4+
int x = 0;
5+
if (i > 0) {
6+
x++;
7+
}
8+
else
9+
{
10+
x--;
11+
}
12+
return x + 1000;
13+
}
14+
}

‎jbmc/regression/jbmc/JumpSimplification/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--show-goto-functions --function Test.foo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
8+
--
9+
IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
10+
^warning: ignoring

‎jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
assert3.class
3+
--throw-assertion-error --disable-uncaught-exception-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎jbmc/regression/jbmc/assert7/Test.class

300 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/assert7/Test.java

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
class Test
2+
{
3+
public static void main(String[] args)
4+
{
5+
AssertionError a = new AssertionError();
6+
if(false)
7+
throw a;
8+
}
9+
}

‎jbmc/regression/jbmc/assert7/test.desc

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

‎jbmc/regression/jbmc/catch1/catch1.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/catch1/test.desc

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
CORE
22
catch1.class
33

4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
^VERIFICATION FAILED$
7+
^\[.*\] no uncaught exception: FAILURE$
78
--
89
^warning: ignoring

‎jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
catch1.class
3+
--disable-uncaught-exception-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎jbmc/regression/jbmc/exceptions18/test.desc

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
CORE
22
Test.class
33
--function Test.goo
4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
^VERIFICATION FAILED$
7+
no uncaught exception: FAILURE
78
--
89
^warning: ignoring

‎jbmc/regression/jbmc/exceptions23/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test.class
44
^EXIT=10$
55
^SIGNAL=0$
66
VERIFICATION FAILED
7-
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 12: FAILURE
7+
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 13: FAILURE
88
--
99
^warning: ignoring
1010
--

‎jbmc/regression/jbmc/exceptions24/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test.class
44
^EXIT=10$
55
^SIGNAL=0$
66
VERIFICATION FAILED
7-
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 10: FAILURE
7+
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 11: FAILURE
88
--
99
^warning: ignoring
1010
--

‎jbmc/regression/jbmc/finally1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
6+
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 10: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally3/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS
7-
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: SUCCESS
7+
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 23: FAILURE
88
^VERIFICATION FAILED$
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/finally4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE
6+
assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 8: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE
6+
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 13: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally7/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS
7-
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: SUCCESS
7+
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 26: FAILURE
88
^VERIFICATION FAILED$
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/generic_class_bound1/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ Gn.class
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block 1: FAILED
7-
.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED
8-
.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED
9-
.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
6+
.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED
7+
.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block .: FAILED
8+
.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block .: FAILED
9+
.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block .: SATISFIED
1010
--
1111
--
1212
This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable

‎jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
8-
assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
9-
assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS
7+
assertion at file Main\.java line 5 function .* bytecode-index 7: FAILURE
8+
assertion at file Main\.java line 6 function .* bytecode-index 15: FAILURE
9+
assertion at file Main\.java line 12 function .* bytecode-index 32: SUCCESS
1010
\*\* 2 of .* failed
1111
--
1212
^warning: ignoring

‎jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
7+
assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
7+
assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
7+
assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
7+
assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
8-
assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
7+
assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
8+
assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
99
\*\* 2 of .* failed
1010
--
1111
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
8-
assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
7+
assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
8+
assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
99
\*\* 2 of .* failed
1010
--
1111
^warning: ignoring

‎jbmc/regression/jbmc/reachability-slice/test2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
A.class
3-
--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
3+
--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
44
1001
55
1002
66
1003

0 commit comments

Comments
 (0)