Move zero_initializer to util

tautschnig · tautschnig · commit 475e4d49b229 · 2018-05-22T15:02:21.000+01:00
This is really just expression-generating code, it isn't specific to linking in
any way. Get rid of the dependency on ansi-c/expr2c by using format().
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -21,13 +21,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_language.h"
 #include "java_utils.h"
 
-#include <util/c_types.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
-
-#include <linking/zero_initializer.h>
 #include <util/suffix.h>
+#include <util/zero_initializer.h>
 
 class java_bytecode_convert_classt:public messaget
 {
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -31,8 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
-
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/class_hierarchy.h>
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
@@ -13,8 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/unicode.h>
-
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 #include "java_pointer_casts.h"
 #include "java_types.h"
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -11,12 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/fresh_symbol.h>
 #include <util/nondet_bool.h>
 #include <util/pointer_offset_size.h>
+#include <util/zero_initializer.h>
 
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
-#include <linking/zero_initializer.h>
-
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
 
diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp
@@ -11,11 +11,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include "java_types.h"
 #include "java_utils.h"
 
-#include <linking/zero_initializer.h>
-
 #include <util/arith_tools.h>
 #include <util/namespace.h>
 #include <util/unicode.h>
+#include <util/zero_initializer.h>
 
 #include <iomanip>
 #include <sstream>
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -14,14 +14,13 @@ Author: Peter Schrammel
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
-#include <linking/zero_initializer.h>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_cast.h>
 #include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
+#include <util/zero_initializer.h>
 
 class remove_java_newt : public messaget
 {
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_typecheck_base.h"
 
 #include <util/config.h>
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 #include "ansi_c_declaration.h"
 
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
@@ -19,8 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/string_constant.h>
 #include <util/type_eq.h>
-
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 #include "anonymous_member.h"
 
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
@@ -16,8 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/source_location.h>
 #include <util/symbol.h>
+#include <util/zero_initializer.h>
 
-#include <linking/zero_initializer.h>
 #include <ansi-c/c_typecast.h>
 
 #include "expr2cpp.h"
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
@@ -20,11 +20,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/pointer_offset_size.h>
+#include <util/zero_initializer.h>
 
 #include <ansi-c/c_qualifiers.h>
 
-#include <linking/zero_initializer.h>
-
 #include "cpp_exception_id.h"
 #include "cpp_type2name.h"
 #include "expr2cpp.h"
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
@@ -14,8 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
-
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 /// Initialize an object with a value
 void cpp_typecheckt::convert_initializer(symbolt &symbol)
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
@@ -17,11 +17,11 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2017
 #include <util/magic.h>
 #include <util/run.h>
 #include <util/tempfile.h>
+#include <util/zero_initializer.h>
 
 #include <json/json_parser.h>
 
 #include <linking/static_lifetime_init.h>
-#include <linking/zero_initializer.h>
 
 #include <goto-programs/read_goto_binary.h>
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -19,8 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
-
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
@@ -17,8 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.h>
-
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 inline static typet c_sizeof_type_rec(const exprt &expr)
 {
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <linking/zero_initializer.h>
+#include <util/zero_initializer.h>
 
 void goto_symext::symex_start_thread(statet &state)
 {
diff --git a/src/linking/Makefile b/src/linking/Makefile
@@ -1,7 +1,6 @@
 SRC = linking.cpp \
       remove_internal_symbols.cpp \
       static_lifetime_init.cpp \
-      zero_initializer.cpp \
       # Empty last line
 
 INCLUDES= -I ..
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
@@ -11,19 +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/namespace.h>
 #include <util/prefix.h>
-
-#include <util/c_types.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/zero_initializer.h>
 
 #include <goto-programs/goto_functions.h>
 
-#include "zero_initializer.h"
-
 bool static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
diff --git a/src/util/Makefile b/src/util/Makefile
@@ -98,6 +98,7 @@ SRC = arith_tools.cpp \
       xml.cpp \
       xml_expr.cpp \
       xml_irep.cpp \
+      zero_initializer.cpp \
       # Empty last line
 
 INCLUDES= -I ..
diff --git a/src/util/zero_initializer.cpp b/src/util/zero_initializer.cpp
@@ -1,24 +1,24 @@
 /*******************************************************************\
 
-Module: Linking: Zero Initialization
+Module: Zero Initialization
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 /// \file
-/// Linking: Zero Initialization
+/// Zero Initialization
 
 #include "zero_initializer.h"
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
-#include <util/message.h>
-#include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/std_expr.h>
-
-#include <ansi-c/expr2c.h>
+#include "arith_tools.h"
+#include "c_types.h"
+#include "format_expr.h"
+#include "format_type.h"
+#include "message.h"
+#include "namespace.h"
+#include "pointer_offset_size.h"
+#include "std_expr.h"
 
 class zero_initializert:public messaget
 {
@@ -41,16 +41,6 @@ class zero_initializert:public messaget
 protected:
   const namespacet &ns;
 
-  std::string to_string(const exprt &src)
-  {
-    return expr2c(src, ns);
-  }
-
-  std::string to_string(const typet &src)
-  {
-    return type2c(src, ns);
-  }
-
   exprt zero_initializer_rec(
     const typet &type,
     const source_locationt &source_location);
@@ -137,15 +127,14 @@ exprt zero_initializert::zero_initializer_rec(
       {
         error().source_location=source_location;
         error() << "failed to zero-initialize array of non-fixed size `"
-                << to_string(array_type.size()) << "'" << eom;
+                << format(array_type.size()) << "'" << eom;
         throw 0;
       }
 
       if(array_size<0)
       {
         error().source_location=source_location;
-        error() << "failed to zero-initialize array of with negative size"
-                << eom;
+        error() << "failed to zero-initialize array with negative size" << eom;
         throw 0;
       }
 
@@ -167,15 +156,14 @@ exprt zero_initializert::zero_initializer_rec(
     {
       error().source_location=source_location;
       error() << "failed to zero-initialize vector of non-fixed size `"
-              << to_string(vector_type.size()) << "'" << eom;
+              << format(vector_type.size()) << "'" << eom;
       throw 0;
     }
 
     if(vector_size<0)
     {
       error().source_location=source_location;
-      error() << "failed to zero-initialize vector of with negative size"
-              << eom;
+      error() << "failed to zero-initialize vector with negative size" << eom;
       throw 0;
     }
 
@@ -299,8 +287,7 @@ exprt zero_initializert::zero_initializer_rec(
   else
   {
     error().source_location=source_location;
-    error() << "failed to zero-initialize `" << to_string(type)
-            << "'" << eom;
+    error() << "failed to zero-initialize `" << format(type) << "'" << eom;
     throw 0;
   }
 }
diff --git a/src/util/zero_initializer.h b/src/util/zero_initializer.h
@@ -1,18 +1,18 @@
 /*******************************************************************\
 
-Module: Linking: Zero Initialization
+Module: Zero Initialization
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 /// \file
-/// Linking: Zero Initialization
+/// Zero Initialization
 
-#ifndef CPROVER_LINKING_ZERO_INITIALIZER_H
-#define CPROVER_LINKING_ZERO_INITIALIZER_H
+#ifndef CPROVER_UTIL_ZERO_INITIALIZER_H
+#define CPROVER_UTIL_ZERO_INITIALIZER_H
 
-#include <util/expr.h>
+#include "expr.h"
 
 class message_handlert;
 class namespacet;
@@ -30,4 +30,4 @@ exprt zero_initializer(
   const source_locationt &,
   const namespacet &);
 
-#endif // CPROVER_LINKING_ZERO_INITIALIZER_H
+#endif // CPROVER_UTIL_ZERO_INITIALIZER_H
