From 683d821f06f178a7e294aa094c584a447740d1e5 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 27 Feb 2018 12:44:12 +0000
Subject: [PATCH] move ansi-c/string_constant.h to util/

---
 src/ansi-c/Makefile                             |  1 -
 src/ansi-c/ansi_c_entry_point.cpp               | 11 +++++------
 src/ansi-c/c_nondet_symbol_factory.cpp          |  9 ++++-----
 src/ansi-c/c_typecheck_expr.cpp                 |  2 +-
 src/ansi-c/c_typecheck_initializer.cpp          |  8 ++++----
 src/ansi-c/literals/convert_string_literal.cpp  |  3 +--
 src/ansi-c/scanner.l                            |  2 +-
 src/cpp/cpp_typecheck_resolve.cpp               |  8 ++++----
 src/goto-analyzer/taint_analysis.cpp            |  5 ++---
 src/goto-instrument/function.cpp                |  5 ++---
 src/goto-instrument/thread_instrumentation.cpp  |  3 +--
 src/goto-programs/builtin_functions.cpp         | 17 ++++++++---------
 src/goto-programs/remove_asm.cpp                |  2 +-
 src/java_bytecode/java_bytecode_parser.cpp      |  7 +++----
 src/java_bytecode/java_entry_point.cpp          | 15 +++++++--------
 src/jsil/parser.y                               |  3 +--
 src/solvers/cvc/cvc_conv.cpp                    |  7 +++----
 src/solvers/flattening/boolbv.cpp               | 13 ++++++-------
 .../string_constraint_generator_constants.cpp   |  2 +-
 .../string_constraint_generator_main.cpp        |  3 ++-
 src/solvers/smt1/smt1_conv.cpp                  | 15 +++++++--------
 src/solvers/smt2/smt2_conv.cpp                  |  7 +++----
 src/util/Makefile                               |  1 +
 src/{ansi-c => util}/string_constant.cpp        |  6 +++---
 src/{ansi-c => util}/string_constant.h          |  9 ++++-----
 25 files changed, 75 insertions(+), 89 deletions(-)
 rename src/{ansi-c => util}/string_constant.cpp (96%)
 rename src/{ansi-c => util}/string_constant.h (86%)

diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index 53e8104aac1..559bff9603d 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -35,7 +35,6 @@ SRC = anonymous_member.cpp \
       padding.cpp \
       preprocessor_line.cpp \
       printf_formatter.cpp \
-      string_constant.cpp \
       type2name.cpp \
       # Empty last line
 
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 47dfd3e03d3..486ef7a1f8a 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -11,18 +11,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <cstdlib>
 
-#include <util/namespace.h>
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
-#include <util/std_code.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/namespace.h>
 #include <util/prefix.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/string_constant.h>
 #include <util/symbol.h>
 
-#include <util/c_types.h>
-#include <ansi-c/string_constant.h>
-
 #include <goto-programs/goto_functions.h>
 #include <linking/static_lifetime_init.h>
 
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 6c3a4265a5e..7bb51962cd8 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -17,17 +17,16 @@ Author: DiffBlue Limited. All rights reserved.
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
-#include <util/std_types.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
 
 #include <linking/zero_initializer.h>
 
-#include <ansi-c/string_constant.h>
-
 #include <goto-programs/goto_functions.h>
 
 /// Create a new temporary static symbol
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 57a55a27c89..f78b49cfea1 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -22,12 +22,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
 #include <util/std_expr.h>
+#include <util/string_constant.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
 #include "c_typecast.h"
 #include "c_qualifiers.h"
-#include "string_constant.h"
 #include "anonymous_member.h"
 #include "padding.h"
 
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index da5a1ce073c..6fea7bc9c77 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -13,15 +13,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/type_eq.h>
-#include <util/std_types.h>
-#include <util/simplify_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
+#include <util/simplify_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
+#include <util/type_eq.h>
 
 #include <linking/zero_initializer.h>
 
-#include "string_constant.h"
 #include "anonymous_member.h"
 
 void c_typecheck_baset::do_initializer(
diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp
index 7167bdd8175..b115697badf 100644
--- a/src/ansi-c/literals/convert_string_literal.cpp
+++ b/src/ansi-c/literals/convert_string_literal.cpp
@@ -16,8 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/unicode.h>
-
-#include "../string_constant.h"
+#include <util/string_constant.h>
 
 #include "unescape_string.h"
 
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 1511da8fbf3..05ded108347 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -19,10 +19,10 @@
 static int isatty(int) { return 0; }
 #endif
 
+#include <util/string_constant.h>
 #include <util/unicode.h>
 
 #include "preprocessor_line.h"
-#include "string_constant.h"
 
 #include "literals/convert_float_literal.h"
 #include "literals/convert_integer_literal.h"
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index ea116ba3952..6689627a7f4 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -14,13 +14,13 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <cstdlib>
 #include <algorithm>
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/prefix.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
 
-#include <util/c_types.h>
-#include <ansi-c/string_constant.h>
 #include <ansi-c/anonymous_member.h>
 
 #include "cpp_typecheck.h"
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
index 44dd30a0c72..f2722c98e91 100644
--- a/src/goto-analyzer/taint_analysis.cpp
+++ b/src/goto-analyzer/taint_analysis.cpp
@@ -14,11 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <fstream>
 
+#include <util/json.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
-#include <util/json.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
 
 #include <goto-programs/class_hierarchy.h>
 
diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp
index 938f0e83db1..4c2b5f598ec 100644
--- a/src/goto-instrument/function.cpp
+++ b/src/goto-instrument/function.cpp
@@ -12,12 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "function.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
-
-#include <util/c_types.h>
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
 
 code_function_callt function_to_call(
   symbol_tablet &symbol_table,
diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp
index c02d9360612..8f92261e90b 100644
--- a/src/goto-instrument/thread_instrumentation.cpp
+++ b/src/goto-instrument/thread_instrumentation.cpp
@@ -9,8 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "thread_instrumentation.h"
 
 #include <util/c_types.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
 
 #include <goto-programs/goto_model.h>
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 60fe569f845..540323bd952 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -13,25 +13,24 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/rational.h>
-#include <util/replace_expr.h>
-#include <util/rational_tools.h>
-#include <util/source_location.h>
 #include <util/cprover_prefix.h>
+#include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
-#include <util/arith_tools.h>
+#include <util/rational.h>
+#include <util/rational_tools.h>
+#include <util/replace_expr.h>
 #include <util/simplify_expr.h>
+#include <util/source_location.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
+#include <util/string_constant.h>
 #include <util/symbol.h>
-#include <util/pointer_predicates.h>
-#include <util/pointer_offset_size.h>
 
 #include <linking/zero_initializer.h>
 
-#include <ansi-c/string_constant.h>
-
 #include <langapi/language_util.h>
 
 #include "format_strings.h"
diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp
index 98af6d6867c..0a514d04487 100644
--- a/src/goto-programs/remove_asm.cpp
+++ b/src/goto-programs/remove_asm.cpp
@@ -18,8 +18,8 @@ Date:   December 2014
 
 #include <util/c_types.h>
 #include <util/std_expr.h>
+#include <util/string_constant.h>
 
-#include <ansi-c/string_constant.h>
 #include <assembler/assembler_parser.h>
 
 class remove_asmt
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
index 85c63e263b5..3c45f87c399 100644
--- a/src/java_bytecode/java_bytecode_parser.cpp
+++ b/src/java_bytecode/java_bytecode_parser.cpp
@@ -13,13 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <string>
 
-#include <util/parser.h>
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
+#include <util/parser.h>
 #include <util/prefix.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/std_expr.h>
+#include <util/string_constant.h>
 
 #include "java_bytecode_parse_tree.h"
 #include "java_types.h"
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 2bf4e8ec9e6..fb5561ae1c9 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -16,20 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <linking/static_lifetime_init.h>
 
 #include <util/arith_tools.h>
-#include <util/prefix.h>
-#include <util/std_types.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
+#include <util/c_types.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/message.h>
-#include <util/config.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
 #include <util/suffix.h>
 
-#include <util/c_types.h>
-#include <ansi-c/string_constant.h>
-
 #include <goto-programs/remove_exceptions.h>
 
 #include "java_object_factory.h"
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
index 2823337d76f..5ea1e3e866b 100644
--- a/src/jsil/parser.y
+++ b/src/jsil/parser.y
@@ -13,8 +13,7 @@ extern char *yyjsiltext;
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
 
 #include "jsil_y.tab.h"
 /*** token declaration **************************************************/
diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index 47008f4f7b5..4762bf64215 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -14,13 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
 #include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 #include <util/string2int.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
 
 void cvc_convt::print_assignment(std::ostream &out) const
 {
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 1f67010402d..245941c0404 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -12,18 +12,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <set>
 
-#include <util/symbol.h>
-#include <util/mp_arith.h>
 #include <util/arith_tools.h>
 #include <util/magic.h>
-#include <util/replace_expr.h>
-#include <util/std_types.h>
+#include <util/mp_arith.h>
 #include <util/prefix.h>
+#include <util/replace_expr.h>
 #include <util/std_expr.h>
-#include <util/threeval.h>
+#include <util/std_types.h>
 #include <util/string2int.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
+#include <util/symbol.h>
+#include <util/threeval.h>
 
 #include "boolbv_type.h"
 
diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp
index 0ed64b37a95..e4411078c81 100644
--- a/src/solvers/refinement/string_constraint_generator_constants.cpp
+++ b/src/solvers/refinement/string_constraint_generator_constants.cpp
@@ -11,8 +11,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <solvers/refinement/string_constraint_generator.h>
 
-#include <ansi-c/string_constant.h>
 #include <util/prefix.h>
+#include <util/string_constant.h>
 #include <util/unicode.h>
 
 /// Add axioms ensuring that the provided string expression and constant are
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 77d6d600a68..1d623280dec 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -20,12 +20,13 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <solvers/refinement/string_constraint_generator.h>
 
 #include <limits>
-#include <ansi-c/string_constant.h>
 #include <java_bytecode/java_types.h>
 #include <solvers/refinement/string_refinement_invariant.h>
+
 #include <util/arith_tools.h>
 #include <util/pointer_predicates.h>
 #include <util/ssa_expr.h>
+#include <util/string_constant.h>
 
 string_constraint_generatort::string_constraint_generatort(
   const string_constraint_generatort::infot &info,
diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp
index 4276c55d0d0..da24fead7f5 100644
--- a/src/solvers/smt1/smt1_conv.cpp
+++ b/src/solvers/smt1/smt1_conv.cpp
@@ -14,17 +14,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
-#include <util/fixedbv.h>
-#include <util/pointer_offset_size.h>
 #include <util/base_type.h>
-#include <util/ieee_float.h>
 #include <util/byte_operators.h>
-#include <util/config.h>
 #include <util/c_types.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/config.h>
+#include <util/fixedbv.h>
+#include <util/ieee_float.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 0fc06e7112e..f1b2d2cd127 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -16,17 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/base_type.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/expr_util.h>
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
-#include <util/config.h>
 #include <util/pointer_offset_size.h>
-#include <util/std_types.h>
 #include <util/std_expr.h>
+#include <util/std_types.h>
 #include <util/string2int.h>
-
-#include <ansi-c/string_constant.h>
+#include <util/string_constant.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/util/Makefile b/src/util/Makefile
index f347bd73aae..2eb5dfebce3 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -74,6 +74,7 @@ SRC = arith_tools.cpp \
       std_expr.cpp \
       std_types.cpp \
       string2int.cpp \
+      string_constant.cpp \
       string_container.cpp \
       string_hash.cpp \
       string_utils.cpp \
diff --git a/src/ansi-c/string_constant.cpp b/src/util/string_constant.cpp
similarity index 96%
rename from src/ansi-c/string_constant.cpp
rename to src/util/string_constant.cpp
index 3c083e4c32e..e6f3ec335a1 100644
--- a/src/ansi-c/string_constant.cpp
+++ b/src/util/string_constant.cpp
@@ -8,9 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "string_constant.h"
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
-#include <util/std_expr.h>
+#include "arith_tools.h"
+#include "c_types.h"
+#include "std_expr.h"
 
 string_constantt::string_constantt():
   exprt(ID_string_constant)
diff --git a/src/ansi-c/string_constant.h b/src/util/string_constant.h
similarity index 86%
rename from src/ansi-c/string_constant.h
rename to src/util/string_constant.h
index d991d6409c1..84588b58cd9 100644
--- a/src/ansi-c/string_constant.h
+++ b/src/util/string_constant.h
@@ -6,12 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#ifndef CPROVER_UTIL_STRING_CONSTANT_H
+#define CPROVER_UTIL_STRING_CONSTANT_H
 
-#ifndef CPROVER_ANSI_C_STRING_CONSTANT_H
-#define CPROVER_ANSI_C_STRING_CONSTANT_H
-
-#include <util/std_expr.h>
-#include <util/expr.h>
+#include "std_expr.h"
+#include "expr.h"
 
 class string_constantt:public exprt
 {