Move lazy_goto_modelt to JBMC

Lazy_goto_modelt is currently only used for Java bytecode.
Loading Java classes cannot be shoehorned into
the current interfaces provided by languaget
without a redesign of languaget (which is currently
not desired).
We will therefore special-case Java-style
loading in lazy_goto_modelt until the languaget
interface has been rethought.

Lazy loading support for other languages is not
planned in forseeable future.

Author: peterschrammel

jbmc/src/java_bytecode/Makefile

@@ -43,8 +43,9 @@ SRC = assignments_from_json.cpp \
       java_trace_validation.cpp \
       java_types.cpp \
       java_utils.cpp \
-      lift_clinit_calls.cpp \
       lambda_synthesis.cpp \
+      lazy_goto_model.cpp \
+      lift_clinit_calls.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \
       remove_exceptions.cpp \

…/goto-programs/lazy_goto_functions_map.h …/java_bytecode/lazy_goto_functions_map.hsrc/goto-programs/lazy_goto_functions_map.h renamed to jbmc/src/java_bytecode/lazy_goto_functions_map.h src/goto-programs/lazy_goto_functions_map.h renamed to jbmc/src/java_bytecode/lazy_goto_functions_map.h

@@ -8,8 +8,8 @@
 
 #include <unordered_set>
 
-#include "goto_functions.h"
-#include "goto_convert_functions.h"
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_functions.h>
 
 #include <langapi/language_file.h>
 #include <util/journalling_symbol_table.h>

src/goto-programs/lazy_goto_model.cpp …mc/src/java_bytecode/lazy_goto_model.cppsrc/goto-programs/lazy_goto_model.cpp renamed to jbmc/src/java_bytecode/lazy_goto_model.cpp src/goto-programs/lazy_goto_model.cpp renamed to jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -4,8 +4,9 @@
 /// Model for lazy loading of functions
 
 #include "lazy_goto_model.h"
-#include "read_goto_binary.h"
-#include "rebuild_goto_start_function.h"
+
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <langapi/mode.h>
 

src/goto-programs/lazy_goto_model.h jbmc/src/java_bytecode/lazy_goto_model.hsrc/goto-programs/lazy_goto_model.h renamed to jbmc/src/java_bytecode/lazy_goto_model.h

@@ -8,10 +8,11 @@
 
 #include <langapi/language_file.h>
 
-#include "abstract_goto_model.h"
-#include "goto_model.h"
+#include <goto-programs/abstract_goto_model.h>
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+
 #include "lazy_goto_functions_map.h"
-#include "goto_convert_functions.h"
 
 class optionst;
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -35,23 +35,22 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
 #include <goto-programs/adjust_float_expressions.h>
-#include <goto-programs/lazy_goto_model.h>
-#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
+#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
-#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
-#include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/show_symbol_table.h>
 
 #include <goto-instrument/full_slicer.h>
-#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>
+#include <goto-instrument/reachability_slicer.h>
 
 #include <goto-symex/path_storage.h>
 
@@ -68,6 +67,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/java_multi_path_symex_only_checker.h>
 #include <java_bytecode/java_single_path_symex_checker.h>
 #include <java_bytecode/java_single_path_symex_only_checker.h>
+#include <java_bytecode/lazy_goto_model.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>

jbmc/src/jbmc/jbmc_parse_options.h

@@ -25,8 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_trace.h>
-#include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
+#include <java_bytecode/lazy_goto_model.h>
 
 #include <goto-symex/path_storage.h>
 

jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -17,7 +17,7 @@ Author: Diffblue Ltd.
 #include <util/options.h>
 #include <util/suffix.h>
 
-#include <goto-programs/lazy_goto_model.h>
+#include <java_bytecode/lazy_goto_model.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <util/file_util.h>

src/goto-programs/Makefile

@@ -28,7 +28,6 @@ SRC = adjust_float_expressions.cpp \
       interpreter_evaluate.cpp \
       json_expr.cpp \
       json_goto_trace.cpp \
-      lazy_goto_model.cpp \
       link_goto_model.cpp \
       link_to_library.cpp \
       loop_ids.cpp \