Skip to content

Commit b127c46

Browse files
author
Owen Jones
committed
Squashed 'cbmc/' changes from 207b801..7202003
7202003 Merge branch 'develop' of github.com:diffblue/cbmc into CBMC_subtree_2018-04-10 768e8a6 Merge pull request diffblue#2009 from romainbrenguier/solvers/sparse-arrays-in-get 69f6e7b Merge pull request diffblue#2032 from tautschnig/replace-rename-performance ec43b00 Merge pull request diffblue#2026 from tautschnig/sat-clean 64b336a Refactor interval_sparse_array::concretize 5392645 Reserve size of array in concretize 8277e92 Stop using concretize_array_expr in unit tests 1a08772 Tests where model involves long strings a6c4010 Stop using concretize_arrays_in_expression 6d87233 Use concretize instead of fill_in_array 052d503 Use get_array in get_char_array_and_concretize 8ed138b Remove unused header c58ac60 Avoid copy in ranged for loops over expressions beff419 Use sparse arrays in get_array 9b286d9 Use sparse arrays in string_refinement::get 037f631 Refactor string_refinementt::get dfc584a Add concretize function for interval_sparse_array cb10550 Use sparse arrays in substitute_array_access ce4c008 Remove plus_exprt_with_overflow_check 4779b25 Get rid of calls to plus_exprt_with_overflow c40b836 Truncate string concatenations in case of overflow c52c813 Add a sum_overflows function 0d03591 Add an `at` function for access in sparse arrays 848dd95 Add an interval_sparse_array::of_expr function 5f07bf0 Initialization of sparse array from array-list 5b4d618 Reduce number of constraints in format ede2fa1 Clear string_dependencies in calls to dec_solve d483c81 Initialize sparse array from array_exprt a914153 Use map instead of vector for sparse array entries 20d2445 Remove unused rename(expr, old_id, new_id) 430d402 Use exprt::depth_iterator in rename_symbolt 54e5b85 Use a const expr to avoid unnecessary detach 6f71ff6 replace_symbolt: stop early if there is nothing to replace with 1dbb162 Clean locally built SAT solver objects 28c076b Merge pull request diffblue#2013 from LAJW/lajw/java-no-load-class e6a9127 Merge pull request diffblue#2020 from tautschnig/sat-cleanup 70741ff Remove support for Precosat 2aa81eb Remove support for SMVSAT a0fd3f7 Remove support for Limmat as a SAT solver 28cca9c Remove unused DIMACS parser 1d81306 Merge pull request diffblue#2015 from tautschnig/fix-smt2_solver-clean 392144d Makefiles: Place .d suffix used for dependencies in DEPEXT variable 839d32a smt2_solver.{o,d} should be removed by "make clean" 48e427a Merge pull request diffblue#1979 from romainbrenguier/regression/fix-indexOf-test c2f3726 Merge pull request diffblue#1976 from romainbrenguier/regression/activate-dependency-tests 42ecfa2 Add --java-no-load-class option 69fb74a Merge pull request diffblue#1995 from tautschnig/byte-update-soundness aa766ae Set string-max-length in indexOf test 988b818 Merge pull request diffblue#1990 from tautschnig/missing-header 8300147 Abort on byte_update(pointer) 4a8d9b4 Include missing header a695814 Merge pull request diffblue#1986 from thk123/revert/1816/overlay-classes 9933b58 Revert "Merge pull request diffblue#1816 from NathanJPhillips/feature/overlay-methods" cd9b839 Revert "Merge pull request diffblue#1982 from NathanJPhillips/bugfix/load-object-once" 58beeb4 Merge pull request diffblue#1978 from svorenova/lambda_tg2478_cont 1e3a9cd Merge pull request diffblue#1980 from NathanJPhillips/tests/irept 772b603 Merge pull request diffblue#1982 from NathanJPhillips/bugfix/load-object-once 0902ae7 Tests to demonstrate expected sharing behaviour of irept 2239ec1 Unit test of irept's public API 81ac259 Prevent test running on symex-driven lazy loading eae194f Allow incorrect paths for jar files on the classpath without crashing 6749fd0 Tests to ensure invalid values in the classpath are ignored 3c95aa1 Prevent attempting to load any class more than once c520331 Unit test to show java.lang.Object can be loaded from an explicit model 05a7b4a Merge pull request diffblue#1981 from smowton/smowton/cleanup/missing-docstring e4dc2aa Merge pull request diffblue#1946 from thk123/feature/TG-1811/unit-tests-for-invokedynamic-static-lambda 2b53d3b Merge pull request diffblue#1983 from svorenova/lambda_tg2478_fix f428247 Tidying up for lambdas f3b1379 Merge pull request diffblue#1975 from romainbrenguier/bugfix/literal-length-TG2878 7d4441d Regression test for lambda in a package 7366fda Format class name for lambda method handles 7db42c0 Add missing Doxygen parameter description 31fa0fe Addressing review comments 2a0927c Merge pull request diffblue#1643 from NathanJPhillips/bugfix/string-solver-function-type-mistake 229d1ee Merge pull request diffblue#1977 from romainbrenguier/bugfix/string-equals-TG-2179 97a6713 Merge pull request diffblue#1816 from NathanJPhillips/feature/overlay-methods e2d4b09 Updates for merge 674c9f0 Activate tests for StringBuffer concat in loops a997ffb Add verification test for String.equals 1ab596d Merge commit '3b8120f3a8c9ed3a343493a44ac454ae265946c1' into develop f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327 55d36b5 Fix code for String.equals baf33f8 Added regression tests 9984fc1 Add ability to overlay classes with new definitions of existing methods 66c529c Tidied up java_class_loader_limitt 397c14e Correcting typos and adding documentation to unit tests 54f1c54 Adding checks for the super class of the generated class df895d3 Temp checkin for checking components 44a5dcb Adding check for inheritance 28bfc37 Amending path to reflect new location e27151b Correcting typo in the scenario name d7356be Modified behaviour to find function calls ac33761 Use raw strings to avoid unnecessary escaping 4201db9 Adding tests for static lambdas f9adaa6 Adding tests for member methods 5f5994b Pull out the logic for getting the inital assignment 7f843a7 Add natural language explanation of the test's checks fa27117 Introduce tests for lambdas that are member variables 8999cf6 Added utiltity for getting this member components 3e0e12e Adding tests for the other two returning lambdas that don't capture f3ddee6 Adding tests to verify the return of the lambda wrapper method db6756e Adding checks for parameters of the called function d2ed92b Adding test for lambda taking array parameters d171f64 Swap finding variable values to use regex 99c21ed Extended find pointer assignment to take a regex 5610aca Added unit test for lambda assigned 7b0cee1 Refactored test method to allow reuse bea730d Adding utility for verifying a set of statements contains a function call ee2179c Introduce checks the the function body for Execute calls the correct lambda 2348d10 Adding unit test for checking local lambda conversion 46fa176 Extending require utilities to be used in test 6df8d6b Extended require_goto_statements to provide meaningful errors 39282a6 Add debug information for working directory 770eb2a Remove methods without a implementation or usage 5cbb758 Merge pull request diffblue#1937 from svorenova/lambda_tg2711 8cfd9bf Merge pull request diffblue#1968 from smowton/smowton/cleanup/remove-exceptions-clarity 6ca3272 Merge pull request diffblue#1973 from karkhaz/kk-c++2a-fixes 212da75 Making members of a test utility class non-const d57fe53 Renaming the folder with lambda unit tests 823f2a7 Adding a unit test for lambda method handles in class symbol 8b172b4 Adding a utility function for lambda method handles in struct 844bb20 Pulling out a utility function to a separate file 3585f73 Updating unit tests for parsing lambda method table 078dc0f Updating a utility function a8ac3d4 Pass lambda method handles to method instruction conversion bf04c93 Add lambda method handles during class conversion a518393 Introduce lambda method handles in java class type 37afd9a Store the full method reference of lambda method handles 0a49697 Store bootstrap method index for invokedynamic instructions 56c9c02 Add test for string literals length af958f0 Correct length field of string literals a190534 Remove-exceptions: make lambda types explicit b052a4d Fix warnings emitted by C++2a compiler 20eaf21 Fix type of call to forName git-subtree-dir: cbmc git-subtree-split: 7202003985a99fb6563cf4d0fb8e7f2c727cc040
1 parent 3b8120f commit b127c46

File tree

163 files changed

+2845
-1694
lines changed

Some content is hidden

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

163 files changed

+2845
-1694
lines changed

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

164 Bytes
Binary file not shown.

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

1.41 KB
Binary file not shown.

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

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

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

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

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

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

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

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

572 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)