Merge pull request #6507 from diffblue/move_goto_check_java

move goto_check_java.h/.cpp to the Java frontend

Author: kroening

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -108,8 +108,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/goto_check_java.h>
-
+#include <java_bytecode/goto_check_java.h>
 #include <java_bytecode/java_bytecode_language.h>
 
 class abstract_goto_modelt;

jbmc/src/java_bytecode/Makefile

@@ -9,6 +9,7 @@ SRC = assignments_from_json.cpp \
       expr2java.cpp \
       generic_parameter_specialization_map.cpp \
       generic_parameter_specialization_map_keys.cpp \
+      goto_check_java.cpp \
       jar_file.cpp \
       jar_pool.cpp \
       java_bmc_util.cpp \

src/analyses/goto_check_java.cpp renamed to jbmc/src/java_bytecode/goto_check_java.cpp

@@ -41,8 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include "guard.h"
-#include "local_bitvector_analysis.h"
+#include <analyses/local_bitvector_analysis.h>
 
 class goto_check_javat
 {
@@ -84,7 +83,6 @@ class goto_check_javat
   const namespacet &ns;
   std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
   goto_programt::const_targett current_target;
-  guard_managert guard_manager;
   messaget log;
 
   /// Check an address-of expression:

src/analyses/goto_check_java.h renamed to jbmc/src/java_bytecode/goto_check_java.h

@@ -19,8 +19,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language.h>
 
-#include <analyses/goto_check_java.h>
-
 #include <goto-checker/bmc_util.h>
 
 #include <goto-programs/class_hierarchy.h>
@@ -29,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/strings/string_refinement.h>
 
+#include <java_bytecode/goto_check_java.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_trace_validation.h>
 

jbmc/src/jbmc/jbmc_parse_options.h

@@ -12,7 +12,7 @@ Author: Peter Schrammel
 #ifndef CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
 #define CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
 
-#include <analyses/goto_check_java.h>
+#include <java_bytecode/goto_check_java.h>
 
 #include <util/parse_options.h>
 #include <util/timestamper.h>

jbmc/src/jdiff/jdiff_parse_options.h

@@ -14,7 +14,6 @@ SRC = ai.cpp \
       global_may_alias.cpp \
       goto_check.cpp \
       goto_check_c.cpp \
-      goto_check_java.cpp \
       goto_rw.cpp \
       guard_bdd.cpp \
       guard_expr.cpp \

src/analyses/Makefile

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_check.h"
 
 #include "goto_check_c.h"
-#include "goto_check_java.h"
 
 #include <util/symbol.h>
 
@@ -30,11 +29,6 @@ void goto_check(
     goto_check_c(
       function_identifier, goto_function, ns, options, message_handler);
   }
-  else if(function_symbol.mode == ID_java)
-  {
-    goto_check_java(
-      function_identifier, goto_function, ns, options, message_handler);
-  }
 }
 
 void goto_check(
@@ -44,7 +38,6 @@ void goto_check(
   message_handlert &message_handler)
 {
   goto_check_c(ns, options, goto_functions, message_handler);
-  goto_check_java(ns, options, goto_functions, message_handler);
 }
 
 void goto_check(
@@ -53,5 +46,4 @@ void goto_check(
   message_handlert &message_handler)
 {
   goto_check_c(options, goto_model, message_handler);
-  goto_check_java(options, goto_model, message_handler);
 }