Port improvements from test-gen-support to master

[tautschnig]

I'm mainly opening this issue to understand whether this is any plan or strategy to do this, or whether this isn't even planned at all. It seems test-gen-support has a large array of improvements in the Java front-end that do not appear to be particularly specific to test generation.

[tautschnig]

Here's a task list, in chronological order, with commit series to be read from top to bottom:

• d47d503 Get symbol of member expression
• 27153d1 Auxiliary function to check if the ssa has enough data to build an identifier
• 2987406 Bitwise operators for mpinteger
• d81dd75 Auxiliary function to retrieve tail of trace and added dead command to trace
• 7fb8174 Fix arithmetic shift operators
• fb616c5 Added a new class for handling the internals
• fc756f3 Adding more symbols that should be excluded
• 2f5b866 Autocomplete script for bash
• 0cf34af Support for Java assume
• 1436e39 Regression tests for Java assume
• 5c30907 Remove assume as coverage target
• e55f20b output covered lines as CSV in show_properties
• 2ae1f47 compress list of lines into line ranges
• f5f47a7 add regression test for coverage lines
• 02d2b9d fix problem with missing comma / range fix for reaching end
• b7d828b Updated dump-C to use the new class
• Migrate Test-gen support #579 (8ae50cd) Port of changes to test-gen-support to master (1) #1123
• fef1fed update interpreter
• Migrate Update interpreter #580 (60744ee) Port of changes to test-gen-support to master (2) #1124
• 1aede78 Preprocessing of goto programs for string refinement
• 3a2e210 Moving is_java_string_type functions to string_preprocess
• 70af9ce Moving refined_string_type to util
• 2929d7f Removed distinction between c string type and refined string type
• 5cb0e5e Removed mention of c string type
• Migrate String refine preprocessing #669 (e81a5e0) Port of changes to test-gen-support to master (3) #1125
• 72ad6ad Making add_string_type more generic
• c9ff379 new identifier for converting char pointer to array
• a04dc21 Many corrections in preprocessing of strings
• bdbeaf5 Many corrections in string refinement
• 6958a56 Need to assign length before calls since it can be overwritten by functions with side-effect
• Migrate Corrections to the string solver #675 (e4e26d8)
• df36fec const refs and clean up
• Migrate Corrections on PR 675 #688 (a11a70b)
• 6cc1266 Adding refined_string_type to util Makefile
• 402f8e1 Adding string preprocessing of goto-programs to Makefile
• 0558291 Adding string solver cpp files to Makefile
• c7328e2 Adding the string refinement option to the CBMC solvers
• 9d2a115 Change option name to --refine-strings
• Migrate String refine option #676 (3eeb73d)
• c7691a4 Restructuration of tests on strings
• Migrate String regression test restructuration #678 (c3cc872)
• 2e62c66 New class for sparse vectors in util
• 5d2919b Interpreter: switch to sparse vector memory map
• 1b97f3d Add support for unbounded-size objects
• Migrate Interpreter sparse memory #689 (28fb701)
• 072e374 Display dynamic object names as 'data' in JSON traces
• Migrate Port JSON pointer output fix #717 (2499213)
• a5f7739 set internal for specific variables in the counterexample trace for test-gen-support
• 5081310 added internal field to json output
• Migrate set internal field in specific variables in the counterexample trace for test-gen-support #709 (932d7df)
• 9ddfb30 Add includes to sparse_vector.h
• Migrate Fix a build issue with test-gen (sparse_vector.h) #742 (6b5d9b7)
• da849ee Adding conversion for functions of the Java Character library
• dead022 Corrected type problem for the function Character.forDigit:(II)C
• Migrate Adding conversion for functions of the Java Character library #699 (03891c9)
• 6c1f700 Adding options to cbmc for parameters of the string solver
• d5c6ac6 Added option to the string solver for string length and printability
• 91d07b1 Bug corrections in string refinement
• Migrate Test gen support string additional options 2 #738 (8081a9a)
• 4c4d85c Implement function-only coverage
• 161aeee Apply review comments to coverage code
• Migrate Cover-function-only support #758 (372bafb)
• 4615184 Restore array skip-initialize flag
• Migrate Restore array skip-initialize flag #789 (051a245)
• 7e1b382 Set function member for class identifier assignment
• Migrate Set function member for class identifier assignment #794 (788a60e)
• 3cb035e Fix style to silence cpplint
• Migrate Fix style to silence cpplint (test-gen-support) #799 (cb065bf)
• 44041ae Allowing some options for string refinement
• Migrate Allowing some options for string refinement #790 (4bebee9)
• 2fc6f09 Preserve true array type in Java -> GOTO conversion. Fixes Incorrect verification failed when threads write to adjacent memory #184.
• Migrate Preserve true array type in Java -> GOTO conversion. Fixes #184. #788 (75337a2)
• 318ab86 Improve class_typet's base description
• 668f30f Always convert methods in two phases, even in eager mode
• 85b1e4f Invoke static initializers on demand
• c631419 Add tests for static initialization order
• Migrate Run clinit methods on demand. Fixes commons-io coverage. #796 (b048787)
• 5851f63 Order string functions in alphabetical order
• Migrate Order string functions in alphabetical order #800 (e05353e)
• 03667af Make add_axioms_from_bool add concret constraints
• aaa56bb Adding tests for issue diffblue/test-gen#119
• 621f366 Correct a mistake in the signature for String.valueOf
• Migrate Fix issue testgen#119 #802 (72e3e35)
• 02f8697 Adding overflow checks in the parsing of integer (dump-c: do not output dead instructions #172)
• Migrate Fix issue test-gen#172 #805 (cc3e3cc)
• f0004a5 Corrections on generated axioms
• 94e9c64 Various improvements in string refinement
• Migrate Various improvements in string refinement #806 (57f5927)
• 718683f Remove trace_stackt
• Migrate Remove trace_stackt #813 (fcafa41)
• 035ae92 Restore array-set for nondet arrays
• Migrate Restore array-set for nondet arrays #820 (935825e)
• 083d8a6 Always report exceptinal output in __CPROVER_start
• Migrate Always report exception output in __CPROVER_start #814 (2f5a391)
• 3c5ae1a Allow checkcast of null pointer
• Migrate Allow checkcast of null pointer #821 (e81b1d9)
• 77ac3a2 Fix Java object factory recursion set
• Migrate Fix Java object factory recursion set #824 (58f3c44)
• 241dbee Add org.cprover package and makefile
• f85494b Add remove_java_nondet
• 19c8d8d Suppress loading methods with nondet signatures
• dc94557 Rearrange loop in remove_java_nondet
• f4a47f9 Split java nondet pass in two
• ff72ddc Ensure assume only throws upon predicate failure
• Migrate Add support for explicit nondet in java code #691 (3fddf20)
• 8ad72a7 Fix linter complaint
• Migrate Fix linter complaint #866 (f5aa612)
• c195e63 Remove 'erase' in replace_java_nondet.cpp
• 6deaa3b Remove skip in replace_java_nondet.cpp
• d15d842 Fix indentation in convert_nondet
• Migrate Remove 'erase' in replace_java_nondet.cpp, fixes #850 #860 (d117475)
• 520cf38 Handle typecast when evaluating addresses in the interpreter
• Migrate Handle typecast when evaluating addresses in the interpreter #854 (468ad17)
• b8586a6 Move coverage arg-parsing into cover.cpp
• Migrate Move coverage arg-parsing into cover.cpp #857 (30b5c72)
• 21eeb29 Enable working smoke tests
• 7cf1c92 Fixes in pre-processing for issue Bug in --dump-c when there is "continue" statement inside a loop #170
• Migrate Fixes in pre-processing for issue #170 #822 (64c8bdf)
• 6b24ec7 Implement StringBuffer methods
• Migrate Implement StringBuffer methods #843 (6c626c7)
• 2c78d46 Correcting constraints for conversion from int diffblue/test-gen#241
• Migrate Fix issue #241 - Conversion from int #840 (0bc3416)
• 9584465 Correction in add_axioms_for_set_length
• Migrate Fix issue #244 - add_axioms_for_set_length #841 (aa78fc1)
• 072ed0f Overhaul of string concretization
• Migrate Fix issue #158 (missing test cases) #819 (f8f7610)
• 0e5a54e Avoid initializing the index set if not needed diffblue/test-gen#199
• Migrate Improve performance by avoiding init of index set #844 (fe03a6e)
• df1caca Adding namespace to arguments of from_expr in debug diffblue/test-gen#201
• Migrate Fix issue cbmc/test-gen#201 #829 (34a847c)
• 6d1feea Set the bytecode index for the instrumentation in goto_check.cpp
• 6796135 Added the bytecode index to the expected result of the regression tests
• Migrate Set the bytecode index for the instrumentation in goto_check.cpp #848 (2dc8cf3)
• 1e9123f Always initialise the exceptional return variable of the entry function
• Migrate Always initialise the exceptional return variable of the entry function #856 (c503366)
• 43e324f Added new friend to bmc to handle refactoring
• Migrate Added new friend to bmc to handle refactoring #901 (f22a696)
• f4ba652 Fix signed/unsigned comparison warning
• Migrate Dup of #873 targeting test-gen-support #938 (05d1ec6)
• 539db25 Fix use-after-free bugs
• Migrate Fix use-after-free bugs in string refinement #939 (f791fef)
• 013f442 Add missing swap instruction
• Migrate Add missing swap instruction #942 (be3f761)
• 8510374 Revert "Remove variable that is always false"
• Migrate Update test-gen-support from master #941 (a54d806)
• eff658a Add hanlded for constant strings
• 06837c8 Use the member functions to make code more robust
• 575b343 Adding simple test for trace correctness
• Migrate Bugfix/trace missing class info #958 (927e48c)
• b6e193e Adding accessors for the access properties
• Migrate Adding accessors for the access properties #975 (d0ec242)
• d437833 Added an uncaught exceptions analysis
• 047671b add the uncaught exceptions analysis to the Makefile
• ca693b4 Make sure that both the caller and callee have exceptional return vars before instrumenting function calls
• 47cd927 Ignore AssertionError This is ignored when we comoute the set of escaped exceptions as well as when replacing throws.
• 229817d Remove duplicate version of class_hierarchyt::get_children_trans_rec
• f42cc33 Addressed reviewers comments
• Migrate Uncaught exceptions analysis #940 (c07cdf9)
• 37c0a36 Avoid marking main function call / arguments as internal
• Migrate Avoid marking main function call / arguments as internal #960 (671193c)
• befb6e2 Fix a mistake in java_identifier_start
• Migrate Fix a mistake in convert_is_java_identifier_start #943 (0bbfffd)
• 8f120bd Declaring auxiliary function for allocation of dynamic objects
• af2fd46 Replacement of string preprocessing for Java
• 45a0260 Merging string and character preprocess as one argument of bytecode conversion
• 7653a76 Removing and deactivating the old preprocessing
• Migrate Complete overhaul of preprocessing of Java strings #906 (5b5a4d2)
• b2dd3a2 Disallow null pointer in data field of String
• Migrate Disallow null pointer in data field of String #900 (00bb9b1)
• 1162377 Specification for contains in the case of a constant argument diffblue/test-gen#159
• Migrate Specification for contains in the case of a constant argument #828 (12c5f26)
• e3b44c7 Avoid copies of string preprocess objects
• 0cc5ae6 Using delete to forbid copies of objects
• Migrate Forbid copies of string preprocess #980 (f05ea17)
• 86de08f Update strings-smoke-test
• 56800d5 Add strings-smoke-tests to regression Makefile
• Migrate Test gen strings update regression #976 (f4f4c44)
• eb9a789 Correcting addition of symbol to symbol map
• Migrate Correcting addition of symbol to symbol map #837 (ac71afe)
• 0dcb773 Change the step at which we replace String methods code
• ca32a0a Removing string conversion from method conversion
• dcf7614 Correcting replace_string_methods to not overwrite the map we iterate on
• 65f2e36 Overwrite String type
• Migrate Overwrite String functions in final step of bytecode conversion #983 (ff81171)
• f9199a0 Make index_of precise diffblue/test-gen#77
• bc59d0c Making lastIndexOf precise diffblue/test-gen#77
• 4f4df8e Optimize last_index_of for constant argument
• 9b11653 Updating comments for index_of and last_index_of on characters
• bc3eedc Replacing str and substring by haystack and needle
• 666bec0 Removing comments about lastIndexOf being imprecise
• 1eb3263 Making comments about the output more precise
• 68cdc6f Renaming str and substring to haystack and needle
• 2d16c2c Correct comments and axioms in lastIndexOf
• f3f5a19 Replacing str and substring by haystack and needle in the comments
• a4ab7db Updating comments for functions adding axioms for index_of
• 1eb7d74 Uniformising mathematical notations in comments
• 069da51 Typo in comment
• 7edfe0d Typo in comment
• 3e9668a Correcting a mistake, universal variable was used in non-quantified formula
• b06476c Correcting indentation in the comments
• af98378 Correcting misuse of univ variable qvar instead of qvar2
• 80dff96 Correcting lower bound in axiom added for last_index_of
• d4a9b2a More comments on the output of last_index_of functions
• 94f99b5 Adding forgotten precondition in not_contains constraint
• cf5b5d3 Update regressions tests for indexOf and lastIndexOf
• Migrate Make String.indexOf and String.lastIndexOf precise #978 (2120a44)
• 7dc5efa Adding a mode option to json output diffblue/test-gen#294
• d41448f Call to lookup that does not throw when symbol is not found
• 62d355c Use the from_type function to get string for the type
• fd80fe6 Adding assertion to make sure "type" field is always set
• b0b8bbc Adding assertions to prevent the "data" field from not being set
• 2c27b41 Assertion to forbid calling json() with nil values
• Migrate Adding java_type field in json for bit vector values #889 (d475cf1)
• c61d095 Improve constructor and copy of strings
• Migrate Improve constructor and copy of strings #993 (07001e9)
• 985baf1 Take care of cases where the symbol exists in table diffblue/test-gen#480
• 9936ddb Improvements following review on PR#995
• Migrate When adding String type, take care of cases where the symbol exists in table #995 (4b9f42e)
• 7707287 Always push the current exceptional return variable on the stack before converting an exception handler
• bb9c28a Added regression test capturing an exception handler that does not start with astore
• 8f629b6 Addressed reviewers comments
• Migrate Remove assumptions about exception handlers #996 (a308fb5)
• 72b611a Improvements on lengths
• 1613290 Update smoke tests for String.length
• Migrate Improve length handling in string preprocessing #994 (2105ee9)
• 01e9e67 Using unique pointers to avoid memory leak in json for expressions
• Migrate Delete language pointer created by get_language_from_mode #1006 (3d80c6f)
• e9e3989 Providing code for Object.getClass() in bytecode conversion
• db1cd5f Cleaning the initialization of string expressions from constants
• Migrate Code for Object.getClass in bytecode conversion #945 (1a3eb1c)
• 4324bbd Disable warnings that result from array-of with zero length
• Migrate Smowton/merge/master 20170614 #1012 (23e2c9b)
• e1aadeb Write traces to status() not cout
• Migrate Write traces to status() not cout #1003 (38907fc)
• 0ee4933 Add simple time limiting to prop_conv and propt
• Migrate Add simple time limiting to prop_conv and propt #1004 (c50f3d5)
• 7cf8d5f Add support for recording and propagating class access flags
• Migrate Add support for recording and propagating class access flags #1000 (6fa72c8)
• f88f461 Remove stray include accidentally merged from master
• Migrate Remove stray include accidentally merged from master #1014 (2d97393)
• 4701c0b Change two errors to warnings
• Migrate Change two errors to warnings #1037 (448f1ca)
• 2534b80 Handling incomplete traces.
• Migrate Instrumenting special assert in CPROVER_START after call into the function under test. (#398) #1018 (eeac672)
• 092f8e2 Lazy methods: fault in static initializer if a static method is called
• Migrate Lazy methods: fault in static initializer if a static method is called #1044 (e6e7e16)
• 471254c Fix win32 compilation
• Migrate Fix test-gen-support win32 compilation #1045 (8cf48d3)
• ce83039 Replace std::cout for errors with messaget::error()
• Migrate Replace std::cout for errors with messaget::error() #1047 (cf0875a)
• 5323702 Fix bad return type of char pointer func
• Migrate Fix bad return type of char pointer func #1048 (f84d96b)
• 1e567fb Add an add_axioms_for_concat_substr function
• 334ab00 Comment in description of test for String.replace()
• ef5bd4d Modifications to doxygen
• cf39c29 Replace asserts
• Migrate Add add_axioms_for_concat_substr #1001 (a9de859)
• 02b7942 Simplifying expressions of the form &array[0] in json
• f4fa778 Simplifying array access and expressions with pointer offsets
• 5cfa413 Adding test to check that data field of strings are set in json
• f950ffc Documentation for json_goto_trace in doxygen format
• Migrate Better output of arrays in json #922 (05875e1)
• fbb5724 Declaring string expression symbol for each string_exprt
• 50be530 Removing overflow check in quantified formula
• Migrate Fix small bugs in string support related to Object.getClass #1021 (70a9806)
• c745aa7 Improvements in the code for String.toCharArray in preprocessing
• 0619f05 Better test for String.toCharArray
• Migrate Improvements in the code for String.toCharArray in String preprocessing #1026 (fbe8be8)
• bc968b0 Always pass namespace to from_expr
• Migrate Always pass namespace to from_expr #1051 (9ac5dff)
• b0b21bb Remove functions that are destined to be modelled in Java
• a95e8dc Removing comments on non-supported functions in string preprocessing
• fdb6f2e Ordering functions in alphabetic order in initialize conversion table
• Migrate Remove functions that are destined to be modelled in Java #992 (0610b0d)
• 6a156a9 Making toLowerCase more precise
• 5553652 Improving the test for Java case functions
• 695b3ce Add comments about characters transformed by toLowerCase
• Migrate Improvements in String.toLowerCase #1036 (71ace43)
• 0e5b254 Java frontend: Set source locations on instructions in code_blocks
• Migrate Java frontend: Set source locations on instructions in code_blocks #1055 (d68f137)
• 33fc907 Call remove-skip before coverage instrumentation
• Migrate Remove skips before cover annotation #1056 (7583da2)
• 20e4def Add preformatted message flag
• Migrate Add preformatted message flag #1059 (406a6c4)
• 913de98 check for java bytecode index in the existing coverage
• a63f2bb replaced assertion by invariant in cover.cpp
• Migrate check for java bytecode index in the existing coverage #772 (71b3fd2)
• 6b6f6cb Add message for unknown cbmc option
• Migrate Add message for unknown cbmc option #910 (f690a3c)
• edd7b0a Fix remove_pointer_offsets
• Migrate Fix remove_pointer_offsets #1066 (a857372)
• fde9c76 Correcting assertions.
• Migrate Refactor gen_nondet_init #990 (77bda4e)
• 9bb474d Fixes parameter detection on bytecode->goto translation
• 0968e93 Regression tests: java method parameter detection
• 1e68ad2 Documentation: functionality around setup_local_variables
• Migrate Documentation to existing code + fixes parameter detection on bytecode->goto translation #1053 (6c0fcda)
• 70d0cb0 Forgotten premise in add_axioms_from_int
• 8a80310 Correcting when to do overflow check in add_axioms_from_int
• 15e88e7 Making tests for int to string conversion more precise
• 7fa229b Update comments in add_axioms_from_int to reflect changes in the code
• fb3ab81 Using PRECONDITION instead of assert
• eaad100 Comment on the bound for overflow in int to string conversion
• 4440343 Adding tests for String.valueOf(long)
• 20f3951 Correction of line numbers in valueOf(long) test
• Migrate Corrects integer/long conversion to string and add tests for StringBuilder.append(long)  #1033 (4a2876b)
• 9c94cb3 Correcting initialization of floatbv_typecast_exprt
• d8af6b6 Adding id for scientific notation of floats
• 5f28dc6 New file for conversion between floats and strings
• 518efa4 Conversion between string and float moved into a new file
• 685a105 Improving the float to string conversion in the preprocessing
• 4ecec1a Improve the documentation of the string preprocessing
• 8367ff5 Allocate array in String result of String.valueOf(F)
• 6518369 Adding test for the String.valueOf(F) function
• 5c71733 Comment corrections in string_constraint_generator_concat
• a8b1e8e Changing assert for PRECONDITION and UNREACHABLE in float to string conversion
• 105925a Comment corrections in string_constraint_generator_float
• 4eacbd3 Renaming add_axioms_from_float to add_axioms_for_string_of_float
• cae6d27 Style improvements in string_constraint_generator_float.cpp
• 64558ca Update comments in string_constraint_generator_valueof.cpp
• e1f2d77 Adding tests for String.valueOf float
• Migrate Pull request/float to string conversion #1017 (d325431)
• d299ea2 Allow "unknown" value assignments in JSON trace
• 82642b9 Add regression test for nil assigns in JSON trace
• Migrate Fix/revert assert non nil decl assign json trace #1050 (56307d0)
• af4edae Fixing inheritance issue for java programs.
• Migrate Fixing inheritance issue for java programs. #1064 (b63547f)
• 0e4176d Fix modes in java entry point code
• 5409f56 Add missing header guard endif comment
• Migrate Fix modes in java entry point code #1079 (6a18c24)
• cf26008 Discard LVT if bytecode > codet translation cannot make sense of it
• 5330536 Documentation for java_bytecode_convert_methodt::variable
• a1af44f Regression tests: groovyc lvts
• Migrate Fall back to anonlocal:: local variables for goto functions if LVT contains unexpected entries #1067 (2a7e25c)
• 50732ee Create is_digit_with_radix()
• 4e5d8cc add_axioms_for_parse_int can take optional radix
• 238c02f Add parseInt with radix to preprocessing
• Migrate Feature/parse int#613 #1077 (3d41879)
• 72677f2 Add regression test for runtime exceptions instrumentation
• 961c0a3 Refactoring the runtime exception instrumentation out of java_bytecode_convert
• a6d1084 Move generate_class_stub out of java_bytecode_convert_classt and to java_utils.cpp and use it to generate stubs for exceptions
• 236e442 Adjusted runtime exceptions regression tests
• Migrate Refactor runtime exception instrumentation #1019 (8226c5b)
• 87ff9de Fixed function inversion.
• cd29f68 Extended check_axioms for not_contains and refactored
• 05516bb Added regresion test for indexOf
• Migrate Fixed: Bug in String.indexOf() #612 #1071 (7c415e8)
• f5f122e Added lower bound in lastIndexOf
• bb31bb5 Added regression test for lastIndexOf
• Migrate Fixed: Investigate performance of lastIndexOf #614 #1076 (c242674)
• 8495451 For contains, added bounds for substring index in !contains case
• 939fb87 Added regression tests based on originating test-gen tests
• Migrate For contains, added bounds for substring index in !contains case #1078 (530a2dd)
• ca3dbab check_class_cast: don't duplicate existing assertion
• 73bd18d Don't throw ClassCastException when casting null pointer
• Migrate Accept null pointer casts #1098 (a3e7557)
• eb3b64c Ensure source locations are assigned to all expressions
• Migrate Ensure source locations are kept across code instrumentation #1088 (6c7d6d4)
• 41bb0d4 Store in the class_typet whether the class is abstract
• 4193022 Added unit tests to demonstrate the abstract flag
• Migrate Mark abstract classes as such  #1084 (9419454)
• 280c45b Declare malloc-site symbol before use
• 8082795 Add test checking that string content is declared before being allocated
• Migrate Declare malloc-site symbols before they are used #1103 (836be74)
• 07ff02d Removing string literal function from string preprocess cpp
• c33306a Removing string_literal declaration
• Migrate Removing string literal function from string preprocess cpp #1102 (f8131c3)
• e2dea9b Correcting type in add axiom for int
• Migrate Correcting type in add axiom for int #1106 (79c0aaa)
• 735065c Make Long.parseLong work
• Migrate Make Long.parseLong work #1097 (a64e6ed)
• bb108a3 Call get_language_options on --show-parse-tree
• Migrate Call get_language_options on --show-parse-tree #1113 (98488bf)
• 8dcff58 Code tidy changes
• a904f08 Add class for randomly selecting a concrete child of an abstract class
• d5513db Make class derived from object factory
• 78a4e05 Made the random selection alphabetical instead of random
• 2c79f51 Removed extra code and just combined into gen_nondet_pointer_init
• e4ac6e2 Modified definition of abstract to not fall over on void* types
• 90286a8 Adding regression tests showing the modified gen code works
• 248ec8e Don't require pointers point to classes
• a3f7eed Made jsonArrays test less strict
• e2e670e Removing whitespace that causes an error on windows
• Migrate Select concrete class for abstract types #1100 (da1dc29)
• d0d046a Add call-graph inversion function
• Migrate Add call-graph invert function #1112 (db0b1f2)
• 728bbc3 Consider implicit exceptions when building the CFG from bytecode
• 68f6ccd Adjust regression tests for exceptions: given that we now consider implicit exceptions when building the CFG, there is no need for the redundant explicit throws
• 85b2a6d Added two more tests for runtime exceptions
• Migrate Consider Java implicit exceptions when building the CFG #1096 (2c29180)

[tautschnig]

There is now https://github.com/diffblue/cbmc/tree/rebased-test-gen-support that has all commits in test-gen-support up to e8e20ea, rebased onto current master (d63d2c7). @peterschrammel has more details.

[tautschnig]

FWIW, I have rebased https://github.com/diffblue/cbmc/tree/rebased-test-gen-support to account for #890. Hopefully that one was the last of the across-the-code-base changes.

[tautschnig]

This plan seems to have been shelved. We'll release from develop.