Essential Java dependencies clean up

src/analyses/dependence_graph.cpp

@@ -272,6 +272,7 @@ jsont dep_graph_domaint::output_json(
   const namespacet &ns) const
 {
   json_arrayt graph;
+  json_exprt json;
 
   for(const auto &cd : control_deps)
   {

src/ansi-c/README.md

@@ -25,7 +25,7 @@ various threading interfaces.
 
 \section preprocessing Preprocessing & Parsing
 
-In the \ref ansi-c and \ref java_bytecode directories
+In the \ref ansi-c directories
 
 **Key classes:**
 * \ref languaget and its subclasses
@@ -46,7 +46,7 @@ digraph G {
 
 \section type-checking Type-checking
 
-In the \ref ansi-c and \ref java_bytecode directories.
+In the \ref ansi-c directories.
 
 **Key classes:**
 * \ref languaget and its subclasses

src/ansi-c/ansi_c_language.h

@@ -63,6 +63,12 @@ class ansi_c_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override
+  {
+    // does not exist
+    UNREACHABLE;
+  }
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<ansi_c_languaget>(); }
 

src/cbmc/CMakeLists.txt

@@ -16,7 +16,6 @@ target_link_libraries(cbmc-lib
     goto-instrument-lib
     goto-programs
     goto-symex
-    java_bytecode
     json
     langapi
     linking

src/cbmc/Makefile

@@ -17,7 +17,6 @@ SRC = all_properties.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
-      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \

src/cbmc/bmc.h

@@ -19,8 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 #include <util/ui_message.h>
 
-#include <java_bytecode/java_enum_static_init_unwind_handler.h>
-
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 #include <solvers/sat/cnf.h>

src/cbmc/bmc_cover.cpp

@@ -359,7 +359,7 @@ bool bmc_covert::operator()()
         json_result["description"] = json_stringt(goal.description);
 
         if(goal.source_location.is_not_nil())
-          json_result["sourceLocation"] = json(goal.source_location);
+          json_result["sourceLocation"] = json(bmc.ns, goal.source_location.get_function(), goal.source_location);
       }
       json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
       json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
@@ -385,7 +385,7 @@ bool bmc_covert::operator()()
               json_input["id"]=json_stringt(id2string(step.io_id));
               if(step.io_args.size()==1)
                 json_input["value"]=
-                  json(step.io_args.front(), bmc.ns, ID_unknown);
+                  json(bmc.ns, step.pc->function, step.io_args.front());
               json_test.push_back(json_input);
             }
           }

src/cbmc/show_vcc.cpp

@@ -97,7 +97,7 @@ void bmct::show_vcc_json(std::ostream &out)
 
     const source_locationt &source_location=s_it->source.pc->source_location;
     if(source_location.is_not_nil())
-      object["sourceLocation"]=json(source_location);
+      object["sourceLocation"] = json(ns, s_it->source.pc->function, source_location);
 
     const std::string &s=s_it->comment;
     if(!s.empty())

src/clobber/CMakeLists.txt

@@ -25,7 +25,6 @@ target_link_libraries(clobber-lib
 )
 
 add_if_library(clobber-lib bv_refinement)
-add_if_library(clobber-lib java_bytecode)
 add_if_library(clobber-lib specc)
 add_if_library(clobber-lib php)
 

src/clobber/Makefile

@@ -1,9 +1,9 @@
 SRC = clobber_main.cpp \
       clobber_parse_options.cpp \
       # Empty last line
+
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../cpp/cpp$(LIBEXT) \
-       ../java_bytecode/java_bytecode$(LIBEXT) \
        ../linking/linking$(LIBEXT) \
        ../big-int/big-int$(LIBEXT) \
        ../goto-programs/goto-programs$(LIBEXT) \

src/cpp/cpp_language.h

@@ -75,6 +75,12 @@ class cpp_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override
+  {
+    // TODO: need a synthetic wrapper with a member that holds the type_info
+    UNIMPLEMENTED;
+  }
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<cpp_languaget>(); }
 

src/goto-analyzer/static_verifier.cpp

@@ -11,7 +11,8 @@ Author: Martin Brain, [email protected]
 #include <util/xml.h>
 #include <util/xml_expr.h>
 #include <util/json.h>
-#include <util/json_expr.h>
+
+#include <langapi/language_util.h>
 
 
 /// Runs the analyzer and then prints out the domain
@@ -78,7 +79,7 @@ bool static_verifier(
           ++unknown;
         }
 
-        j["sourceLocation"]=json(i_it->source_location);
+        j["sourceLocation"] = json(ns, i_it->function, i_it->source_location);
       }
     }
     m.status() << "Writing JSON report" << messaget::eom;

src/goto-analyzer/unreachable_instructions.cpp

@@ -16,10 +16,11 @@ Date: April 2016
 #include <sstream>
 
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <util/file_util.h>
 #include <util/xml.h>
 
+#include <langapi/language_util.h>
+
 #include <analyses/cfg_dominators.h>
 
 #include <goto-programs/goto_model.h>
@@ -157,7 +158,7 @@ static void add_to_json(
     // print info for file actually with full path
     json_objectt &i_entry=dead_ins.push_back().make_object();
     const source_locationt &l=it->second->source_location;
-    i_entry["sourceLocation"]=json(l);
+    i_entry["sourceLocation"] = json(ns, it->second->function, l);
     i_entry["statement"]=json_stringt(s);
   }
 }

src/goto-cc/CMakeLists.txt

@@ -19,7 +19,6 @@ target_link_libraries(goto-cc-lib
     langapi
 )
 
-add_if_library(goto-cc-lib java_bytecode)
 add_if_library(goto-cc-lib jsil)
 
 # Executable

src/goto-cc/Makefile

@@ -24,7 +24,6 @@ OBJ += ../big-int/big-int$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
-      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \

src/goto-cc/goto_cc_languages.cpp

@@ -15,7 +15,6 @@ Author: CM Wintersteiger
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
-#include <java_bytecode/java_bytecode_language.h>
 #include <jsil/jsil_language.h>
 
 #ifdef HAVE_SPECC
@@ -26,7 +25,6 @@ void goto_cc_modet::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-  register_language(new_java_bytecode_language);
   register_language(new_jsil_language);
 
   #ifdef HAVE_SPECC

src/goto-diff/goto_diff_base.cpp

@@ -13,9 +13,10 @@ Author: Peter Schrammel
 
 #include <goto-programs/show_properties.h>
 
-#include <util/json_expr.h>
 #include <util/options.h>
 
+#include <langapi/language_util.h>
+
 /// Output diff result
 void goto_difft::output_functions() const
 {
@@ -136,7 +137,7 @@ void goto_difft::convert_function_json(
   const symbolt &symbol = ns.lookup(function_name);
 
   result["name"] = json_stringt(id2string(function_name));
-  result["sourceLocation"] = json(symbol.location);
+  result["sourceLocation"] = json(ns, function_name, symbol.location);
 
   if(options.get_bool_option("show-properties"))
   {

src/goto-programs/Makefile

@@ -52,7 +52,6 @@ SRC = basic_blocks.cpp \
       remove_unused_functions.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
-      replace_java_nondet.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \
       set_properties.cpp \