Merge pull request #3711 from tautschnig/move-json-xml-expr

Move {json,xml}_expr.{h,cpp} to goto-programs [blocks: #3734, #3736]

src/analyses/custom_bitvector_analysis.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
-#include <util/xml_expr.h>
+#include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
 

src/analyses/dependence_graph.cpp

@@ -17,8 +17,7 @@ Date: August 2013
 #include <cassert>
 
 #include <util/container_utils.h>
-#include <util/json.h>
-#include <util/json_expr.h>
+#include <util/json_irep.h>
 
 #include "goto_rw.h"
 

src/cbmc/bmc_cover.cpp

@@ -16,18 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-checker/bmc_util.h>
 
-#include <util/xml.h>
-#include <util/xml_expr.h>
 #include <util/json.h>
 #include <util/json_stream.h>
-#include <util/json_expr.h>
+#include <util/xml_irep.h>
 
 #include <solvers/prop/cover_goals.h>
 #include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
-#include <goto-programs/xml_goto_trace.h>
+
+#include <goto-programs/json_expr.h>
 #include <goto-programs/json_goto_trace.h>
+#include <goto-programs/xml_expr.h>
+#include <goto-programs/xml_goto_trace.h>
 
 #include <langapi/language_util.h>
 

src/cbmc/fault_localization.cpp

@@ -13,12 +13,12 @@ Author: Peter Schrammel
 
 #include <chrono>
 
-#include <util/threeval.h>
 #include <util/arith_tools.h>
-#include <util/symbol.h>
-#include <util/std_expr.h>
 #include <util/message.h>
-#include <util/xml_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol.h>
+#include <util/threeval.h>
+#include <util/xml_irep.h>
 
 #include <solvers/prop/minimize.h>
 #include <solvers/prop/literal_expr.h>

src/goto-analyzer/static_verifier.cpp

@@ -8,7 +8,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include "static_verifier.h"
 
-#include <util/json_expr.h>
+#include <util/json_irep.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/options.h>

src/goto-analyzer/unreachable_instructions.cpp

@@ -14,7 +14,7 @@ Date: April 2016
 #include "unreachable_instructions.h"
 
 #include <util/file_util.h>
-#include <util/json_expr.h>
+#include <util/json_irep.h>
 #include <util/options.h>
 #include <util/xml.h>
 

src/goto-diff/goto_diff_base.cpp

@@ -11,7 +11,7 @@ Author: Peter Schrammel
 
 #include "goto_diff.h"
 
-#include <util/json_expr.h>
+#include <util/json_irep.h>
 #include <util/options.h>
 
 #include <goto-programs/goto_model.h>

src/goto-instrument/unwind.h

@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "unwindset.h"
 
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <goto-programs/goto_model.h>
 
 class goto_modelt;

src/goto-programs/Makefile

@@ -25,6 +25,7 @@ SRC = adjust_float_expressions.cpp \
       instrument_preconditions.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
+      json_expr.cpp \
       json_goto_trace.cpp \
       lazy_goto_model.cpp \
       link_goto_model.cpp \
@@ -67,6 +68,7 @@ SRC = adjust_float_expressions.cpp \
       vcd_goto_trace.cpp \
       wp.cpp \
       write_goto_binary.cpp \
+      xml_expr.cpp \
       xml_goto_trace.cpp \
       # Empty last line
 

src/goto-programs/goto_inline_class.h

@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/message.h>
 #include <util/json.h>
-#include <util/json_expr.h>
 
 #include "goto_functions.h"
 

src/goto-programs/json_expr.cpp

@@ -11,31 +11,29 @@ Author: Peter Schrammel
 
 #include "json_expr.h"
 
-#include "namespace.h"
-#include "expr.h"
-#include "json.h"
-#include "arith_tools.h"
-#include "ieee_float.h"
-#include "fixedbv.h"
-#include "std_expr.h"
-#include "config.h"
-#include "identifier.h"
-#include "invariant.h"
+#include <util/arith_tools.h>
+#include <util/config.h>
+#include <util/expr.h>
+#include <util/fixedbv.h>
+#include <util/identifier.h>
+#include <util/ieee_float.h>
+#include <util/invariant.h>
+#include <util/json.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
 
-#include <langapi/mode.h>
 #include <langapi/language.h>
+#include <langapi/mode.h>
 
 #include <memory>
 
-static exprt simplify_json_expr(
-  const exprt &src,
-  const namespacet &ns)
+static exprt simplify_json_expr(const exprt &src, const namespacet &ns)
 {
-  if(src.id()==ID_constant)
+  if(src.id() == ID_constant)
   {
-    const typet &type=ns.follow(src.type());
+    const typet &type = ns.follow(src.type());
 
-    if(type.id()==ID_pointer)
+    if(type.id() == ID_pointer)
     {
       const constant_exprt &c = to_constant_expr(src);
 
@@ -72,10 +70,10 @@ static exprt simplify_json_expr(
     return simplify_json_expr(
       to_index_expr(to_address_of_expr(src).object()).array(), ns);
   }
-  else if(src.id()==ID_member &&
-          id2string(
-            to_member_expr(src).get_component_name())
-              .find("@")!=std::string::npos)
+  else if(
+    src.id() == ID_member &&
+    id2string(to_member_expr(src).get_component_name()).find("@") !=
+      std::string::npos)
   {
     // simplify expressions of the form  member_expr(object, @class_identifier)
     return simplify_json_expr(to_member_expr(src).struct_op(), ns);
@@ -84,31 +82,6 @@ static exprt simplify_json_expr(
   return src;
 }
 
-json_objectt json(const source_locationt &location)
-{
-  json_objectt result;
-
-  if(!location.get_working_directory().empty())
-    result["workingDirectory"] = json_stringt(location.get_working_directory());
-
-  if(!location.get_file().empty())
-    result["file"] = json_stringt(location.get_file());
-
-  if(!location.get_line().empty())
-    result["line"] = json_stringt(location.get_line());
-
-  if(!location.get_column().empty())
-    result["column"] = json_stringt(location.get_column());
-
-  if(!location.get_function().empty())
-    result["function"] = json_stringt(location.get_function());
-
-  if(!location.get_java_bytecode_index().empty())
-    result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
-
-  return result;
-}
-
 /// Output a CBMC type in json.
 /// The `mode` argument is used to correctly report types.
 /// \param type: a type
@@ -116,81 +89,79 @@ json_objectt json(const source_locationt &location)
 /// \param mode: language in which the code was written; for now ID_C and
 ///   ID_java are supported
 /// \return a json object
-json_objectt json(
-  const typet &type,
-  const namespacet &ns,
-  const irep_idt &mode)
+json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
 {
   if(type.id() == ID_symbol_type)
     return json(ns.follow(type), ns, mode);
 
   json_objectt result;
 
-  if(type.id()==ID_unsignedbv)
+  if(type.id() == ID_unsignedbv)
   {
-    result["name"]=json_stringt("integer");
-    result["width"]=
+    result["name"] = json_stringt("integer");
+    result["width"] =
       json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
   }
-  else if(type.id()==ID_signedbv)
+  else if(type.id() == ID_signedbv)
   {
-    result["name"]=json_stringt("integer");
-    result["width"]=
+    result["name"] = json_stringt("integer");
+    result["width"] =
       json_numbert(std::to_string(to_signedbv_type(type).get_width()));
   }
-  else if(type.id()==ID_floatbv)
+  else if(type.id() == ID_floatbv)
   {
-    result["name"]=json_stringt("float");
-    result["width"]=
+    result["name"] = json_stringt("float");
+    result["width"] =
       json_numbert(std::to_string(to_floatbv_type(type).get_width()));
   }
-  else if(type.id()==ID_bv)
+  else if(type.id() == ID_bv)
   {
-    result["name"]=json_stringt("integer");
-    result["width"]=json_numbert(std::to_string(to_bv_type(type).get_width()));
+    result["name"] = json_stringt("integer");
+    result["width"] =
+      json_numbert(std::to_string(to_bv_type(type).get_width()));
   }
-  else if(type.id()==ID_c_bit_field)
+  else if(type.id() == ID_c_bit_field)
   {
-    result["name"]=json_stringt("integer");
-    result["width"]=
+    result["name"] = json_stringt("integer");
+    result["width"] =
       json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
   }
-  else if(type.id()==ID_c_enum_tag)
+  else if(type.id() == ID_c_enum_tag)
   {
     // we return the base type
     return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
   }
-  else if(type.id()==ID_fixedbv)
+  else if(type.id() == ID_fixedbv)
   {
-    result["name"]=json_stringt("fixed");
-    result["width"]=
+    result["name"] = json_stringt("fixed");
+    result["width"] =
       json_numbert(std::to_string(to_fixedbv_type(type).get_width()));
   }
-  else if(type.id()==ID_pointer)
+  else if(type.id() == ID_pointer)
   {
-    result["name"]=json_stringt("pointer");
+    result["name"] = json_stringt("pointer");
     result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);
   }
-  else if(type.id()==ID_bool)
+  else if(type.id() == ID_bool)
   {
-    result["name"]=json_stringt("boolean");
+    result["name"] = json_stringt("boolean");
   }
-  else if(type.id()==ID_array)
+  else if(type.id() == ID_array)
   {
-    result["name"]=json_stringt("array");
+    result["name"] = json_stringt("array");
     result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
   }
-  else if(type.id()==ID_vector)
+  else if(type.id() == ID_vector)
   {
-    result["name"]=json_stringt("vector");
+    result["name"] = json_stringt("vector");
     result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
-    result["size"]=json(to_vector_type(type).size(), ns, mode);
+    result["size"] = json(to_vector_type(type).size(), ns, mode);
   }
-  else if(type.id()==ID_struct)
+  else if(type.id() == ID_struct)
   {
-    result["name"]=json_stringt("struct");
-    json_arrayt &members=result["members"].make_array();
-    const struct_typet::componentst &components=
+    result["name"] = json_stringt("struct");
+    json_arrayt &members = result["members"].make_array();
+    const struct_typet::componentst &components =
       to_struct_type(type).components();
     for(const auto &component : components)
     {
@@ -199,11 +170,11 @@ json_objectt json(
       members.push_back(std::move(e));
     }
   }
-  else if(type.id()==ID_union)
+  else if(type.id() == ID_union)
   {
-    result["name"]=json_stringt("union");
-    json_arrayt &members=result["members"].make_array();
-    const union_typet::componentst &components=
+    result["name"] = json_stringt("union");
+    json_arrayt &members = result["members"].make_array();
+    const union_typet::componentst &components =
       to_union_type(type).components();
     for(const auto &component : components)
     {
@@ -213,7 +184,7 @@ json_objectt json(
     }
   }
   else
-    result["name"]=json_stringt("unknown");
+    result["name"] = json_stringt("unknown");
 
   return result;
 }
@@ -232,94 +203,91 @@ static std::string binary(const constant_exprt &src)
 /// \param mode: language in which the code was written; for now ID_C and
 ///   ID_java are supported
 /// \return a json object
-json_objectt json(
-  const exprt &expr,
-  const namespacet &ns,
-  const irep_idt &mode)
+json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
 {
   json_objectt result;
 
-  const typet &type=ns.follow(expr.type());
+  const typet &type = ns.follow(expr.type());
 
-  if(expr.id()==ID_constant)
+  if(expr.id() == ID_constant)
   {
     std::unique_ptr<languaget> lang;
-    if(mode==ID_unknown)
-      lang=std::unique_ptr<languaget>(get_default_language());
+    if(mode == ID_unknown)
+      lang = std::unique_ptr<languaget>(get_default_language());
     else
     {
-      lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
+      lang = std::unique_ptr<languaget>(get_language_from_mode(mode));
       if(!lang)
-        lang=std::unique_ptr<languaget>(get_default_language());
+        lang = std::unique_ptr<languaget>(get_default_language());
     }
 
     const typet &underlying_type =
       type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;
 
     std::string type_string;
-    bool error=lang->from_type(underlying_type, type_string, ns);
+    bool error = lang->from_type(underlying_type, type_string, ns);
     CHECK_RETURN(!error);
 
     std::string value_string;
     lang->from_expr(expr, value_string, ns);
 
-    const constant_exprt &constant_expr=to_constant_expr(expr);
-    if(type.id()==ID_unsignedbv ||
-       type.id()==ID_signedbv ||
-       type.id()==ID_c_bit_field)
+    const constant_exprt &constant_expr = to_constant_expr(expr);
+    if(
+      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+      type.id() == ID_c_bit_field)
     {
-      std::size_t width=to_bitvector_type(type).get_width();
+      std::size_t width = to_bitvector_type(type).get_width();
 
-      result["name"]=json_stringt("integer");
+      result["name"] = json_stringt("integer");
       result["binary"] = json_stringt(binary(constant_expr));
-      result["width"]=json_numbert(std::to_string(width));
-      result["type"]=json_stringt(type_string);
-      result["data"]=json_stringt(value_string);
+      result["width"] = json_numbert(std::to_string(width));
+      result["type"] = json_stringt(type_string);
+      result["data"] = json_stringt(value_string);
     }
-    else if(type.id()==ID_c_enum)
+    else if(type.id() == ID_c_enum)
     {
-      result["name"]=json_stringt("integer");
+      result["name"] = json_stringt("integer");
       result["binary"] = json_stringt(binary(constant_expr));
       result["width"] = json_numbert(std::to_string(
         to_bitvector_type(to_c_enum_type(type).subtype()).get_width()));
-      result["type"]=json_stringt("enum");
-      result["data"]=json_stringt(value_string);
+      result["type"] = json_stringt("enum");
+      result["data"] = json_stringt(value_string);
     }
-    else if(type.id()==ID_c_enum_tag)
+    else if(type.id() == ID_c_enum_tag)
     {
       constant_exprt tmp(
         to_constant_expr(expr).get_value(),
         ns.follow_tag(to_c_enum_tag_type(type)));
       return json(tmp, ns, mode);
     }
-    else if(type.id()==ID_bv)
+    else if(type.id() == ID_bv)
     {
-      result["name"]=json_stringt("bitvector");
+      result["name"] = json_stringt("bitvector");
       result["binary"] = json_stringt(binary(constant_expr));
     }
-    else if(type.id()==ID_fixedbv)
+    else if(type.id() == ID_fixedbv)
     {
-      result["name"]=json_stringt("fixed");
+      result["name"] = json_stringt("fixed");
       result["width"] =
         json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
-      result["data"]=
+      result["data"] =
         json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
     }
-    else if(type.id()==ID_floatbv)
+    else if(type.id() == ID_floatbv)
     {
-      result["name"]=json_stringt("float");
+      result["name"] = json_stringt("float");
       result["width"] =
         json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
-      result["data"]=
+      result["data"] =
         json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
     }
-    else if(type.id()==ID_pointer)
+    else if(type.id() == ID_pointer)
     {
-      result["name"]=json_stringt("pointer");
-      result["type"]=json_stringt(type_string);
-      exprt simpl_expr=simplify_json_expr(expr, ns);
+      result["name"] = json_stringt("pointer");
+      result["type"] = json_stringt(type_string);
+      exprt simpl_expr = simplify_json_expr(expr, ns);
       if(
         simpl_expr.get(ID_value) == ID_NULL ||
         // remove typecast on NULL
@@ -327,49 +295,49 @@ json_objectt json(
          simpl_expr.type().id() == ID_pointer &&
          to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
       {
-        result["data"]=json_stringt(value_string);
+        result["data"] = json_stringt(value_string);
       }
-      else if(simpl_expr.id()==ID_symbol)
+      else if(simpl_expr.id() == ID_symbol)
       {
-        const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();
+        const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier();
         identifiert identifier(id2string(ptr_id));
         DATA_INVARIANT(
           !identifier.components.empty(),
           "pointer identifier should have non-empty components");
-        result["data"]=json_stringt(identifier.components.back());
+        result["data"] = json_stringt(identifier.components.back());
       }
     }
-    else if(type.id()==ID_bool)
+    else if(type.id() == ID_bool)
     {
-      result["name"]=json_stringt("boolean");
-      result["binary"]=json_stringt(expr.is_true()?"1":"0");
-      result["data"]=jsont::json_boolean(expr.is_true());
+      result["name"] = json_stringt("boolean");
+      result["binary"] = json_stringt(expr.is_true() ? "1" : "0");
+      result["data"] = jsont::json_boolean(expr.is_true());
     }
-    else if(type.id()==ID_c_bool)
+    else if(type.id() == ID_c_bool)
     {
-      result["name"]=json_stringt("integer");
+      result["name"] = json_stringt("integer");
       result["width"] =
         json_numbert(std::to_string(to_bitvector_type(type).get_width()));
-      result["type"]=json_stringt(type_string);
-      result["binary"]=json_stringt(expr.get_string(ID_value));
-      result["data"]=json_stringt(value_string);
+      result["type"] = json_stringt(type_string);
+      result["binary"] = json_stringt(expr.get_string(ID_value));
+      result["data"] = json_stringt(value_string);
     }
-    else if(type.id()==ID_string)
+    else if(type.id() == ID_string)
     {
-      result["name"]=json_stringt("string");
+      result["name"] = json_stringt("string");
       result["data"] = json_stringt(constant_expr.get_value());
     }
     else
     {
-      result["name"]=json_stringt("unknown");
+      result["name"] = json_stringt("unknown");
     }
   }
-  else if(expr.id()==ID_array)
+  else if(expr.id() == ID_array)
   {
-    result["name"]=json_stringt("array");
-    json_arrayt &elements=result["elements"].make_array();
+    result["name"] = json_stringt("array");
+    json_arrayt &elements = result["elements"].make_array();
 
-    std::size_t index=0;
+    std::size_t index = 0;
 
     forall_operands(it, expr)
     {
@@ -379,21 +347,21 @@ json_objectt json(
       index++;
     }
   }
-  else if(expr.id()==ID_struct)
+  else if(expr.id() == ID_struct)
   {
-    result["name"]=json_stringt("struct");
+    result["name"] = json_stringt("struct");
 
     // these are expected to have a struct type
-    if(type.id()==ID_struct)
+    if(type.id() == ID_struct)
     {
-      const struct_typet &struct_type=to_struct_type(type);
-      const struct_typet::componentst &components=struct_type.components();
+      const struct_typet &struct_type = to_struct_type(type);
+      const struct_typet::componentst &components = struct_type.components();
       DATA_INVARIANT(
-        components.size()==expr.operands().size(),
+        components.size() == expr.operands().size(),
         "number of struct components should match with its type");
 
-      json_arrayt &members=result["members"].make_array();
-      for(std::size_t m=0; m<expr.operands().size(); m++)
+      json_arrayt &members = result["members"].make_array();
+      for(std::size_t m = 0; m < expr.operands().size(); m++)
       {
         json_objectt e({{"value", json(expr.operands()[m], ns, mode)},
                         {"name", json_stringt(components[m].get_name())}});
@@ -401,17 +369,17 @@ json_objectt json(
       }
     }
   }
-  else if(expr.id()==ID_union)
+  else if(expr.id() == ID_union)
   {
-    result["name"]=json_stringt("union");
+    result["name"] = json_stringt("union");
 
-    const union_exprt &union_expr=to_union_expr(expr);
+    const union_exprt &union_expr = to_union_expr(expr);
     result["member"] =
       json_objectt({{"value", json(union_expr.op(), ns, mode)},
                     {"name", json_stringt(union_expr.get_component_name())}});
   }
   else
-    result["name"]=json_stringt("unknown");
+    result["name"] = json_stringt("unknown");
 
   return result;
 }

src/goto-programs/json_expr.h

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Expressions in JSON
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Expressions in JSON
+
+#ifndef CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
+#define CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
+
+#include <util/irep.h>
+#include <util/json.h>
+
+class typet;
+class exprt;
+class namespacet;
+
+json_objectt json(const exprt &, const namespacet &, const irep_idt &mode);
+
+json_objectt json(const typet &, const namespacet &, const irep_idt &mode);
+
+#endif // CPROVER_GOTO_PROGRAMS_JSON_EXPR_H

src/goto-programs/json_goto_trace.cpp

@@ -12,17 +12,15 @@ Author: Daniel Kroening
 /// Traces of GOTO Programs
 
 #include "json_goto_trace.h"
-#include "goto_trace.h"
 
-#include <util/json_expr.h>
-#include <util/json.h>
-#include <util/json_stream.h>
+#include <langapi/language_util.h>
 #include <util/arith_tools.h>
 #include <util/config.h>
 #include <util/invariant.h>
 #include <util/simplify_expr.h>
-#include <util/json_irep.h>
-#include <langapi/language_util.h>
+
+#include "goto_trace.h"
+#include "json_expr.h"
 
 /// Convert an ASSERT goto_trace step.
 /// \param [out] json_failure: The JSON object that

src/goto-programs/json_goto_trace.h

@@ -16,10 +16,10 @@ Date: November 2005
 
 #include "goto_trace.h"
 
-#include <util/json.h>
-#include <util/json_stream.h>
-#include <util/json_expr.h>
 #include <util/invariant.h>
+#include <util/json.h>
+#include <util/json_irep.h>
+#include <util/json_stream.h>
 
 /// This is structure is here to facilitate
 /// passing arguments to the conversion

src/goto-programs/loop_ids.cpp

@@ -13,10 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <iostream>
 
-#include <util/xml.h>
-#include <util/xml_expr.h>
-#include <util/json.h>
-#include <util/json_expr.h>
+#include <util/json_irep.h>
+#include <util/xml_irep.h>
 
 void show_loop_ids(
   ui_message_handlert::uit ui,

src/goto-programs/show_goto_functions.cpp

@@ -13,8 +13,6 @@ Author: Peter Schrammel
 
 #include <util/xml.h>
 #include <util/json.h>
-#include <util/json_expr.h>
-#include <util/xml_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 

src/goto-programs/show_goto_functions_json.cpp

@@ -14,7 +14,6 @@ Author: Thomas Kiley
 #include <iostream>
 #include <sstream>
 
-#include <util/json_expr.h>
 #include <util/json_irep.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>

src/goto-programs/show_goto_functions_xml.cpp

@@ -14,9 +14,9 @@ Author: Thomas Kiley
 #include <iostream>
 #include <sstream>
 
-#include <util/xml_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
+#include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
 

src/goto-programs/show_properties.cpp

@@ -13,10 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <iostream>
 
-#include <util/xml.h>
-#include <util/xml_expr.h>
-#include <util/json.h>
-#include <util/json_expr.h>
+#include <util/json_irep.h>
+#include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
 

src/goto-programs/xml_expr.cpp

@@ -0,0 +1,274 @@
+/*******************************************************************\
+
+Module: Expressions in XML
+
+Author: Daniel Kroening
+
+  Date: November 2005
+
+\*******************************************************************/
+
+/// \file
+/// Expressions in XML
+
+#include "xml_expr.h"
+
+#include <util/arith_tools.h>
+#include <util/config.h>
+#include <util/expr.h>
+#include <util/fixedbv.h>
+#include <util/ieee_float.h>
+#include <util/invariant.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/xml.h>
+
+xmlt xml(const typet &type, const namespacet &ns)
+{
+  if(type.id() == ID_symbol_type)
+    return xml(ns.follow(type), ns);
+
+  xmlt result;
+
+  if(type.id() == ID_unsignedbv)
+  {
+    result.name = "integer";
+    result.set_attribute("width", to_unsignedbv_type(type).get_width());
+  }
+  else if(type.id() == ID_signedbv)
+  {
+    result.name = "integer";
+    result.set_attribute("width", to_signedbv_type(type).get_width());
+  }
+  else if(type.id() == ID_floatbv)
+  {
+    result.name = "float";
+    result.set_attribute("width", to_floatbv_type(type).get_width());
+  }
+  else if(type.id() == ID_bv)
+  {
+    result.name = "integer";
+    result.set_attribute("width", to_bv_type(type).get_width());
+  }
+  else if(type.id() == ID_c_bit_field)
+  {
+    result.name = "integer";
+    result.set_attribute("width", to_c_bit_field_type(type).get_width());
+  }
+  else if(type.id() == ID_c_enum_tag)
+  {
+    // we return the base type
+    return xml(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
+  }
+  else if(type.id() == ID_fixedbv)
+  {
+    result.name = "fixed";
+    result.set_attribute("width", to_fixedbv_type(type).get_width());
+  }
+  else if(type.id() == ID_pointer)
+  {
+    result.name = "pointer";
+    result.new_element("subtype").new_element() =
+      xml(to_pointer_type(type).subtype(), ns);
+  }
+  else if(type.id() == ID_bool)
+  {
+    result.name = "boolean";
+  }
+  else if(type.id() == ID_array)
+  {
+    result.name = "array";
+    result.new_element("subtype").new_element() =
+      xml(to_array_type(type).subtype(), ns);
+  }
+  else if(type.id() == ID_vector)
+  {
+    result.name = "vector";
+    result.new_element("subtype").new_element() =
+      xml(to_vector_type(type).subtype(), ns);
+    result.new_element("size").new_element() =
+      xml(to_vector_type(type).size(), ns);
+  }
+  else if(type.id() == ID_struct)
+  {
+    result.name = "struct";
+    const struct_typet::componentst &components =
+      to_struct_type(type).components();
+    for(const auto &component : components)
+    {
+      xmlt &e = result.new_element("member");
+      e.set_attribute("name", id2string(component.get_name()));
+      e.new_element("type").new_element() = xml(component.type(), ns);
+    }
+  }
+  else if(type.id() == ID_union)
+  {
+    result.name = "union";
+    const union_typet::componentst &components =
+      to_union_type(type).components();
+    for(const auto &component : components)
+    {
+      xmlt &e = result.new_element("member");
+      e.set_attribute("name", id2string(component.get_name()));
+      e.new_element("type").new_element() = xml(component.type(), ns);
+    }
+  }
+  else
+    result.name = "unknown";
+
+  return result;
+}
+
+xmlt xml(const exprt &expr, const namespacet &ns)
+{
+  xmlt result;
+
+  const typet &type = ns.follow(expr.type());
+
+  if(expr.id() == ID_constant)
+  {
+    if(
+      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+      type.id() == ID_c_bit_field)
+    {
+      std::size_t width = to_bitvector_type(type).get_width();
+
+      result.name = "integer";
+      result.set_attribute(
+        "binary", integer2binary(numeric_cast_v<mp_integer>(expr), width));
+      result.set_attribute("width", width);
+
+      const typet &underlying_type = type.id() == ID_c_bit_field
+                                       ? to_c_bit_field_type(type).subtype()
+                                       : type;
+
+      bool is_signed = underlying_type.id() == ID_signedbv;
+
+      std::string sig = is_signed ? "" : "unsigned ";
+
+      if(width == config.ansi_c.char_width)
+        result.set_attribute("c_type", sig + "char");
+      else if(width == config.ansi_c.int_width)
+        result.set_attribute("c_type", sig + "int");
+      else if(width == config.ansi_c.short_int_width)
+        result.set_attribute("c_type", sig + "short int");
+      else if(width == config.ansi_c.long_int_width)
+        result.set_attribute("c_type", sig + "long int");
+      else if(width == config.ansi_c.long_long_int_width)
+        result.set_attribute("c_type", sig + "long long int");
+
+      mp_integer i;
+      if(!to_integer(to_constant_expr(expr), i))
+        result.data = integer2string(i);
+    }
+    else if(type.id() == ID_c_enum)
+    {
+      result.name = "integer";
+      result.set_attribute("binary", expr.get_string(ID_value));
+      result.set_attribute(
+        "width", to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
+      result.set_attribute("c_type", "enum");
+
+      mp_integer i;
+      if(!to_integer(to_constant_expr(expr), i))
+        result.data = integer2string(i);
+    }
+    else if(type.id() == ID_c_enum_tag)
+    {
+      constant_exprt tmp(
+        to_constant_expr(expr).get_value(),
+        ns.follow_tag(to_c_enum_tag_type(type)));
+      return xml(tmp, ns);
+    }
+    else if(type.id() == ID_bv)
+    {
+      result.name = "bitvector";
+      result.set_attribute("binary", expr.get_string(ID_value));
+    }
+    else if(type.id() == ID_fixedbv)
+    {
+      result.name = "fixed";
+      result.set_attribute("width", to_bitvector_type(type).get_width());
+      result.set_attribute("binary", expr.get_string(ID_value));
+      result.data = fixedbvt(to_constant_expr(expr)).to_ansi_c_string();
+    }
+    else if(type.id() == ID_floatbv)
+    {
+      result.name = "float";
+      result.set_attribute("width", to_bitvector_type(type).get_width());
+      result.set_attribute("binary", expr.get_string(ID_value));
+      result.data = ieee_floatt(to_constant_expr(expr)).to_ansi_c_string();
+    }
+    else if(type.id() == ID_pointer)
+    {
+      result.name = "pointer";
+      result.set_attribute("binary", expr.get_string(ID_value));
+      if(expr.get(ID_value) == ID_NULL)
+        result.data = "NULL";
+    }
+    else if(type.id() == ID_bool)
+    {
+      result.name = "boolean";
+      result.set_attribute("binary", expr.is_true() ? "1" : "0");
+      result.data = expr.is_true() ? "TRUE" : "FALSE";
+    }
+    else if(type.id() == ID_c_bool)
+    {
+      result.name = "integer";
+      result.set_attribute("c_type", "_Bool");
+      result.set_attribute("binary", expr.get_string(ID_value));
+      const mp_integer b = numeric_cast_v<mp_integer>(expr);
+      result.data = integer2string(b);
+    }
+    else
+    {
+      result.name = "unknown";
+    }
+  }
+  else if(expr.id() == ID_array)
+  {
+    result.name = "array";
+
+    unsigned index = 0;
+
+    forall_operands(it, expr)
+    {
+      xmlt &e = result.new_element("element");
+      e.set_attribute("index", index);
+      e.new_element(xml(*it, ns));
+      index++;
+    }
+  }
+  else if(expr.id() == ID_struct)
+  {
+    result.name = "struct";
+
+    // these are expected to have a struct type
+    if(type.id() == ID_struct)
+    {
+      const struct_typet &struct_type = to_struct_type(type);
+      const struct_typet::componentst &components = struct_type.components();
+      PRECONDITION(components.size() == expr.operands().size());
+
+      for(unsigned m = 0; m < expr.operands().size(); m++)
+      {
+        xmlt &e = result.new_element("member");
+        e.new_element() = xml(expr.operands()[m], ns);
+        e.set_attribute("name", id2string(components[m].get_name()));
+      }
+    }
+  }
+  else if(expr.id() == ID_union)
+  {
+    const union_exprt &union_expr = to_union_expr(expr);
+    result.name = "union";
+
+    xmlt &e = result.new_element("member");
+    e.new_element(xml(union_expr.op(), ns));
+    e.set_attribute("member_name", id2string(union_expr.get_component_name()));
+  }
+  else
+    result.name = "unknown";
+
+  return result;
+}

src/goto-programs/xml_expr.h

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_XML_EXPR_H
+#define CPROVER_GOTO_PROGRAMS_XML_EXPR_H
+
+#include <util/xml.h>
+
+class typet;
+class exprt;
+class namespacet;
+
+xmlt xml(const exprt &, const namespacet &);
+
+xmlt xml(const typet &, const namespacet &);
+
+#endif // CPROVER_GOTO_PROGRAMS_XML_EXPR_H

src/goto-programs/xml_goto_trace.cpp

@@ -15,12 +15,13 @@ Author: Daniel Kroening
 
 #include <cassert>
 
-#include <util/xml_expr.h>
 #include <util/symbol.h>
+#include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
 
 #include "printf_formatter.h"
+#include "xml_expr.h"
 
 void convert(
   const namespacet &ns,

src/goto-symex/show_vcc.cpp

@@ -20,8 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/exception_utils.h>
 #include <util/format_expr.h>
-#include <util/json.h>
-#include <util/json_expr.h>
+#include <util/json_irep.h>
 #include <util/ui_message.h>
 
 void show_vcc_plain(

src/pointer-analysis/value_set_analysis.cpp

@@ -11,10 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set_analysis.h"
 
-#include <util/prefix.h>
 #include <util/cprover_prefix.h>
-#include <util/xml_expr.h>
-#include <util/xml.h>
+#include <util/prefix.h>
+#include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
 

src/util/Makefile

@@ -37,7 +37,6 @@ SRC = allocate_objects.cpp \
       irep_serialization.cpp \
       invariant_utils.cpp \
       json.cpp \
-      json_expr.cpp \
       json_irep.cpp \
       json_stream.cpp \
       lispexpr.cpp \
@@ -103,7 +102,6 @@ SRC = allocate_objects.cpp \
       validate_types.cpp \
       version.cpp \
       xml.cpp \
-      xml_expr.cpp \
       xml_irep.cpp \
       # Empty last line
 

src/util/json_expr.h

@@ -1,35 +0,0 @@
-/*******************************************************************\
-
-Module: Expressions in JSON
-
-Author: Peter Schrammel
-
-\*******************************************************************/
-
-/// \file
-/// Expressions in JSON
-
-#ifndef CPROVER_UTIL_JSON_EXPR_H
-#define CPROVER_UTIL_JSON_EXPR_H
-
-#include "json.h"
-#include "irep.h"
-
-class source_locationt;
-class typet;
-class exprt;
-class namespacet;
-
-json_objectt json(
-  const exprt &,
-  const namespacet &,
-  const irep_idt &mode);
-
-json_objectt json(
-  const typet &,
-  const namespacet &,
-  const irep_idt &mode);
-
-json_objectt json(const source_locationt &);
-
-#endif // CPROVER_UTIL_JSON_EXPR_H

src/util/json_irep.cpp

@@ -137,3 +137,28 @@ irept json_irept::convert_from_json(const jsont &in) const
 
   return out;
 }
+
+json_objectt json(const source_locationt &location)
+{
+  json_objectt result;
+
+  if(!location.get_working_directory().empty())
+    result["workingDirectory"] = json_stringt(location.get_working_directory());
+
+  if(!location.get_file().empty())
+    result["file"] = json_stringt(location.get_file());
+
+  if(!location.get_line().empty())
+    result["line"] = json_stringt(location.get_line());
+
+  if(!location.get_column().empty())
+    result["column"] = json_stringt(location.get_column());
+
+  if(!location.get_function().empty())
+    result["function"] = json_stringt(location.get_function());
+
+  if(!location.get_java_bytecode_index().empty())
+    result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
+
+  return result;
+}

src/util/json_irep.h

@@ -13,9 +13,9 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 #define CPROVER_UTIL_JSON_IREP_H
 
 #include "irep.h"
+#include "json.h"
 
-class jsont;
-class json_objectt;
+class source_locationt;
 
 class json_irept
 {
@@ -38,4 +38,6 @@ private:
   bool include_comments;
 };
 
+json_objectt json(const source_locationt &);
+
 #endif // CPROVER_UTIL_JSON_IREP_H

src/util/module_dependencies.txt

@@ -1,5 +1,4 @@
 big-int
-langapi # should go away
 mach # system
 malloc # system
 nonstd

src/util/ui_message.cpp

@@ -12,12 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 
 #include "cmdline.h"
-#include "json.h"
-#include "json_expr.h"
+#include "json_irep.h"
 #include "json_stream.h"
 #include "make_unique.h"
-#include "xml.h"
-#include "xml_expr.h"
+#include "xml_irep.h"
 
 ui_message_handlert::ui_message_handlert(
   message_handlert *_message_handler,

src/util/xml_expr.cpp

@@ -1,303 +0,0 @@
-/*******************************************************************\
-
-Module: Expressions in XML
-
-Author: Daniel Kroening
-
-  Date: November 2005
-
-\*******************************************************************/
-
-/// \file
-/// Expressions in XML
-
-#include "xml_expr.h"
-
-#include "arith_tools.h"
-#include "config.h"
-#include "expr.h"
-#include "fixedbv.h"
-#include "ieee_float.h"
-#include "invariant.h"
-#include "namespace.h"
-#include "std_expr.h"
-#include "xml.h"
-
-xmlt xml(const source_locationt &location)
-{
-  xmlt result;
-
-  result.name="location";
-
-  if(!location.get_working_directory().empty())
-    result.set_attribute(
-      "working-directory", id2string(location.get_working_directory()));
-
-  if(!location.get_file().empty())
-    result.set_attribute("file", id2string(location.get_file()));
-
-  if(!location.get_line().empty())
-    result.set_attribute("line", id2string(location.get_line()));
-
-  if(!location.get_column().empty())
-    result.set_attribute("column", id2string(location.get_column()));
-
-  if(!location.get_function().empty())
-    result.set_attribute("function", id2string(location.get_function()));
-
-  return result;
-}
-
-xmlt xml(
-  const typet &type,
-  const namespacet &ns)
-{
-  if(type.id() == ID_symbol_type)
-    return xml(ns.follow(type), ns);
-
-  xmlt result;
-
-  if(type.id()==ID_unsignedbv)
-  {
-    result.name="integer";
-    result.set_attribute("width", to_unsignedbv_type(type).get_width());
-  }
-  else if(type.id()==ID_signedbv)
-  {
-    result.name="integer";
-    result.set_attribute("width", to_signedbv_type(type).get_width());
-  }
-  else if(type.id()==ID_floatbv)
-  {
-    result.name="float";
-    result.set_attribute("width", to_floatbv_type(type).get_width());
-  }
-  else if(type.id()==ID_bv)
-  {
-    result.name="integer";
-    result.set_attribute("width", to_bv_type(type).get_width());
-  }
-  else if(type.id()==ID_c_bit_field)
-  {
-    result.name="integer";
-    result.set_attribute("width", to_c_bit_field_type(type).get_width());
-  }
-  else if(type.id()==ID_c_enum_tag)
-  {
-    // we return the base type
-    return xml(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
-  }
-  else if(type.id()==ID_fixedbv)
-  {
-    result.name="fixed";
-    result.set_attribute("width", to_fixedbv_type(type).get_width());
-  }
-  else if(type.id()==ID_pointer)
-  {
-    result.name="pointer";
-    result.new_element("subtype").new_element() =
-      xml(to_pointer_type(type).subtype(), ns);
-  }
-  else if(type.id()==ID_bool)
-  {
-    result.name="boolean";
-  }
-  else if(type.id()==ID_array)
-  {
-    result.name="array";
-    result.new_element("subtype").new_element() =
-      xml(to_array_type(type).subtype(), ns);
-  }
-  else if(type.id()==ID_vector)
-  {
-    result.name="vector";
-    result.new_element("subtype").new_element() =
-      xml(to_vector_type(type).subtype(), ns);
-    result.new_element("size").new_element()=
-      xml(to_vector_type(type).size(), ns);
-  }
-  else if(type.id()==ID_struct)
-  {
-    result.name="struct";
-    const struct_typet::componentst &components=
-      to_struct_type(type).components();
-    for(const auto &component : components)
-    {
-      xmlt &e=result.new_element("member");
-      e.set_attribute("name", id2string(component.get_name()));
-      e.new_element("type").new_element()=xml(component.type(), ns);
-    }
-  }
-  else if(type.id()==ID_union)
-  {
-    result.name="union";
-    const union_typet::componentst &components=
-      to_union_type(type).components();
-    for(const auto &component : components)
-    {
-      xmlt &e=result.new_element("member");
-      e.set_attribute("name", id2string(component.get_name()));
-      e.new_element("type").new_element()=xml(component.type(), ns);
-    }
-  }
-  else
-    result.name="unknown";
-
-  return result;
-}
-
-xmlt xml(
-  const exprt &expr,
-  const namespacet &ns)
-{
-  xmlt result;
-
-  const typet &type=ns.follow(expr.type());
-
-  if(expr.id()==ID_constant)
-  {
-    if(type.id()==ID_unsignedbv ||
-       type.id()==ID_signedbv ||
-       type.id()==ID_c_bit_field)
-    {
-      std::size_t width=to_bitvector_type(type).get_width();
-
-      result.name="integer";
-      result.set_attribute(
-        "binary", integer2binary(numeric_cast_v<mp_integer>(expr), width));
-      result.set_attribute("width", width);
-
-      const typet &underlying_type = type.id() == ID_c_bit_field
-                                       ? to_c_bit_field_type(type).subtype()
-                                       : type;
-
-      bool is_signed=underlying_type.id()==ID_signedbv;
-
-      std::string sig=is_signed?"":"unsigned ";
-
-      if(width==config.ansi_c.char_width)
-        result.set_attribute("c_type", sig+"char");
-      else if(width==config.ansi_c.int_width)
-        result.set_attribute("c_type", sig+"int");
-      else if(width==config.ansi_c.short_int_width)
-        result.set_attribute("c_type", sig+"short int");
-      else if(width==config.ansi_c.long_int_width)
-        result.set_attribute("c_type", sig+"long int");
-      else if(width==config.ansi_c.long_long_int_width)
-        result.set_attribute("c_type", sig+"long long int");
-
-      mp_integer i;
-      if(!to_integer(to_constant_expr(expr), i))
-        result.data=integer2string(i);
-    }
-    else if(type.id()==ID_c_enum)
-    {
-      result.name="integer";
-      result.set_attribute("binary", expr.get_string(ID_value));
-      result.set_attribute(
-        "width", to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
-      result.set_attribute("c_type", "enum");
-
-      mp_integer i;
-      if(!to_integer(to_constant_expr(expr), i))
-        result.data=integer2string(i);
-    }
-    else if(type.id()==ID_c_enum_tag)
-    {
-      constant_exprt tmp(
-        to_constant_expr(expr).get_value(),
-        ns.follow_tag(to_c_enum_tag_type(type)));
-      return xml(tmp, ns);
-    }
-    else if(type.id()==ID_bv)
-    {
-      result.name="bitvector";
-      result.set_attribute("binary", expr.get_string(ID_value));
-    }
-    else if(type.id()==ID_fixedbv)
-    {
-      result.name="fixed";
-      result.set_attribute("width", to_bitvector_type(type).get_width());
-      result.set_attribute("binary", expr.get_string(ID_value));
-      result.data=fixedbvt(to_constant_expr(expr)).to_ansi_c_string();
-    }
-    else if(type.id()==ID_floatbv)
-    {
-      result.name="float";
-      result.set_attribute("width", to_bitvector_type(type).get_width());
-      result.set_attribute("binary", expr.get_string(ID_value));
-      result.data=ieee_floatt(to_constant_expr(expr)).to_ansi_c_string();
-    }
-    else if(type.id()==ID_pointer)
-    {
-      result.name="pointer";
-      result.set_attribute("binary", expr.get_string(ID_value));
-      if(expr.get(ID_value)==ID_NULL)
-        result.data="NULL";
-    }
-    else if(type.id()==ID_bool)
-    {
-      result.name="boolean";
-      result.set_attribute("binary", expr.is_true()?"1":"0");
-      result.data=expr.is_true()?"TRUE":"FALSE";
-    }
-    else if(type.id()==ID_c_bool)
-    {
-      result.name="integer";
-      result.set_attribute("c_type", "_Bool");
-      result.set_attribute("binary", expr.get_string(ID_value));
-      const mp_integer b = numeric_cast_v<mp_integer>(expr);
-      result.data=integer2string(b);
-    }
-    else
-    {
-      result.name="unknown";
-    }
-  }
-  else if(expr.id()==ID_array)
-  {
-    result.name="array";
-
-    unsigned index=0;
-
-    forall_operands(it, expr)
-    {
-      xmlt &e=result.new_element("element");
-      e.set_attribute("index", index);
-      e.new_element(xml(*it, ns));
-      index++;
-    }
-  }
-  else if(expr.id()==ID_struct)
-  {
-    result.name="struct";
-
-    // these are expected to have a struct type
-    if(type.id()==ID_struct)
-    {
-      const struct_typet &struct_type=to_struct_type(type);
-      const struct_typet::componentst &components=struct_type.components();
-      PRECONDITION(components.size() == expr.operands().size());
-
-      for(unsigned m=0; m<expr.operands().size(); m++)
-      {
-        xmlt &e=result.new_element("member");
-        e.new_element()=xml(expr.operands()[m], ns);
-        e.set_attribute("name", id2string(components[m].get_name()));
-      }
-    }
-  }
-  else if(expr.id()==ID_union)
-  {
-    const union_exprt &union_expr = to_union_expr(expr);
-    result.name="union";
-
-    xmlt &e=result.new_element("member");
-    e.new_element(xml(union_expr.op(), ns));
-    e.set_attribute("member_name", id2string(union_expr.get_component_name()));
-  }
-  else
-    result.name="unknown";
-
-  return result;
-}

src/util/xml_expr.h

@@ -1,30 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-
-#ifndef CPROVER_UTIL_XML_EXPR_H
-#define CPROVER_UTIL_XML_EXPR_H
-
-#include "xml.h"
-
-class source_locationt;
-class typet;
-class exprt;
-class namespacet;
-
-xmlt xml(
-  const exprt &,
-  const namespacet &);
-
-xmlt xml(
-  const typet &,
-  const namespacet &);
-
-xmlt xml(const source_locationt &);
-
-#endif // CPROVER_UTIL_XML_EXPR_H

src/util/xml_irep.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening
 #include <string>
 
 #include "irep.h"
-#include "xml.h"
+#include "source_location.h"
 
 void convert(
   const irept &irep,
@@ -87,3 +87,28 @@ void convert(
     }
   }
 }
+
+xmlt xml(const source_locationt &location)
+{
+  xmlt result;
+
+  result.name = "location";
+
+  if(!location.get_working_directory().empty())
+    result.set_attribute(
+      "working-directory", id2string(location.get_working_directory()));
+
+  if(!location.get_file().empty())
+    result.set_attribute("file", id2string(location.get_file()));
+
+  if(!location.get_line().empty())
+    result.set_attribute("line", id2string(location.get_line()));
+
+  if(!location.get_column().empty())
+    result.set_attribute("column", id2string(location.get_column()));
+
+  if(!location.get_function().empty())
+    result.set_attribute("function", id2string(location.get_function()));
+
+  return result;
+}

src/util/xml_irep.h

@@ -10,8 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_XML_IREP_H
 #define CPROVER_UTIL_XML_IREP_H
 
+#include "xml.h"
+
 class irept;
-class xmlt;
+class source_locationt;
 
 void convert(
   const irept &irep,
@@ -21,4 +23,6 @@ void convert(
   const xmlt &xml,
   irept &irep);
 
+xmlt xml(const source_locationt &);
+
 #endif // CPROVER_UTIL_XML_IREP_H

unit/Makefile

@@ -25,6 +25,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/goto_program_symbol_type_table_consistency.cpp \
        goto-programs/goto_program_table_consistency.cpp \
        goto-programs/goto_trace_output.cpp \
+       goto-programs/xml_expr.cpp \
        goto-symex/ssa_equation.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
@@ -68,7 +69,6 @@ SRC += analyses/ai/ai.cpp \
        util/symbol_table.cpp \
        util/symbol.cpp \
        util/unicode.cpp \
-       util/xml_expr.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.

unit/goto-programs/xml_expr.cpp

@@ -13,7 +13,8 @@ Author: Michael Tautschnig
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
-#include <util/xml_expr.h>
+
+#include <goto-programs/xml_expr.h>
 
 TEST_CASE("Constant expression to XML")
 {