Remove java dependency in string solver

[romainbrenguier]

This removes the dependencies on java_bytecode from the solver (see #1869)

[peterschrammel]

Thanks. That's a good start!
What about the following:

• https://github.com/diffblue/cbmc/blob/develop/src/solvers/refinement/string_constraint_generator.h#L391
• https://github.com/diffblue/cbmc/blob/develop/src/solvers/refinement/string_constraint_generator_format.cpp#L421
• https://github.com/diffblue/cbmc/blob/develop/src/solvers/refinement/string_refinement.cpp#L1126

Are they generic enough to remove the word "java"?

[tautschnig]

The CMake failure highlights that there is a problem in unit/CMakeLists.txt that now needs to be addressed: because of the way the Linux linker works, target_link_libraries now needs to list goto-programs above java_bytecode. Though maybe the problem can also be solved differently:

$ git grep java_lang_object_type
goto-programs/remove_instanceof.cpp:  symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
java_bytecode/java_types.cpp:reference_typet java_lang_object_type()
java_bytecode/java_types.h:reference_typet java_lang_object_type();

Having a single user of java_lang_object_type(), which in turn only picks out the subtype() is weird. Add to that that the single user is outside the java_bytecode folder.

[martin-cs]

Fine once the other issues have been addressed.

[kroening]

Cherry-picked two commits to make this move.

[peterschrammel]

@kroening, the develop build is broken now.
I'm working on the java deps issue in #1935 / #1869.
Cherry-picking without waiting for CI is not the way forward.

[romainbrenguier]

closing as the changes are in develop now