Move {json,xml}_expr.{h,cpp} to goto-programs

There should not be a dependency from util to langapi, and goto-programs is also
the only place where {json,xml}_expr are used.

Author: tautschnig

src/cbmc/bmc_cover.cpp

@@ -17,17 +17,18 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/bmc_util.h>
 
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <util/json_stream.h>
-#include <util/xml_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/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/util/json_expr.cpp renamed to src/goto-programs/json_expr.cpp

@@ -11,16 +11,16 @@ 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/namespace.h>
+#include <util/expr.h>
+#include <util/json.h>
+#include <util/arith_tools.h>
+#include <util/ieee_float.h>
+#include <util/fixedbv.h>
+#include <util/std_expr.h>
+#include <util/config.h>
+#include <util/identifier.h>
+#include <util/invariant.h>
 
 #include <langapi/mode.h>
 #include <langapi/language.h>

src/util/json_expr.h renamed to src/goto-programs/json_expr.h

@@ -9,11 +9,11 @@ Author: Peter Schrammel
 /// \file
 /// Expressions in JSON
 
-#ifndef CPROVER_UTIL_JSON_EXPR_H
-#define CPROVER_UTIL_JSON_EXPR_H
+#ifndef CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
+#define CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
 
-#include "json.h"
-#include "irep.h"
+#include <util/json.h>
+#include <util/irep.h>
 
 class typet;
 class exprt;
@@ -29,4 +29,4 @@ json_objectt json(
   const namespacet &,
   const irep_idt &mode);
 
-#endif // CPROVER_UTIL_JSON_EXPR_H
+#endif // CPROVER_GOTO_PROGRAMS_JSON_EXPR_H

src/goto-programs/json_goto_trace.cpp

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

src/util/xml_expr.cpp renamed to src/goto-programs/xml_expr.cpp

@@ -13,15 +13,15 @@ Author: Daniel Kroening
 
 #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"
+#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,

src/util/xml_expr.h renamed to src/goto-programs/xml_expr.h

@@ -7,10 +7,10 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 
-#ifndef CPROVER_UTIL_XML_EXPR_H
-#define CPROVER_UTIL_XML_EXPR_H
+#ifndef CPROVER_GOTO_PROGRAMS_XML_EXPR_H
+#define CPROVER_GOTO_PROGRAMS_XML_EXPR_H
 
-#include "xml.h"
+#include <util/xml.h>
 
 class typet;
 class exprt;
@@ -24,4 +24,4 @@ xmlt xml(
   const typet &,
   const namespacet &);
 
-#endif // CPROVER_UTIL_XML_EXPR_H
+#endif // CPROVER_GOTO_PROGRAMS_XML_EXPR_H

src/goto-programs/xml_goto_trace.cpp

@@ -16,12 +16,12 @@ Author: Daniel Kroening
 #include <cassert>
 
 #include <util/symbol.h>
-#include <util/xml_expr.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/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/module_dependencies.txt

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

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/util/xml_expr.cpp renamed to 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")
 {