Rename zero_initializer to expr_initializer in preparation of generalisation

tautschnig · tautschnig · commit 2af792903559 · 2018-06-05T09:10:41.000Z
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -23,10 +23,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/std_expr.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
@@ -24,14 +24,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.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
@@ -12,8 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_typecheck.h"
 
 #include <util/arith_tools.h>
+#include <util/expr_initializer.h>
 #include <util/unicode.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
@@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_object_factory.h"
 
+#include <util/expr_initializer.h>
 #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>
diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp
@@ -12,9 +12,9 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include "java_utils.h"
 
 #include <util/arith_tools.h>
+#include <util/expr_initializer.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
@@ -17,10 +17,10 @@ Author: Peter Schrammel
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_cast.h>
+#include <util/expr_initializer.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 <util/zero_initializer.h>
+#include <util/expr_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
@@ -14,12 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_initializer.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 <util/zero_initializer.h>
 
 #include "anonymous_member.h"
 
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
@@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/expr_initializer.h>
 #include <util/source_location.h>
 #include <util/symbol.h>
-#include <util/zero_initializer.h>
 
 #include <ansi-c/c_typecast.h>
 
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
@@ -19,8 +19,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
-#include <util/zero_initializer.h>
 
 #include <ansi-c/c_qualifiers.h>
 
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
@@ -13,8 +13,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/pointer_offset_size.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
@@ -14,10 +14,10 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2017
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/magic.h>
 #include <util/run.h>
 #include <util/tempfile.h>
-#include <util/zero_initializer.h>
 
 #include <json/json_parser.h>
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -16,10 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.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
@@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/invariant_utils.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.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 <util/zero_initializer.h>
+#include <util/expr_initializer.h>
 
 void goto_symext::symex_start_thread(statet &state)
 {
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
@@ -14,11 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
-#include <util/zero_initializer.h>
 
 #include <goto-programs/goto_functions.h>
 
diff --git a/src/util/Makefile b/src/util/Makefile
@@ -11,6 +11,7 @@ SRC = arith_tools.cpp \
       dstring.cpp \
       endianness_map.cpp \
       expr.cpp \
+      expr_initializer.cpp \
       expr_util.cpp \
       file_util.cpp \
       find_macros.cpp \
@@ -98,7 +99,6 @@ 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/expr_initializer.cpp b/src/util/expr_initializer.cpp
@@ -1,15 +1,15 @@
 /*******************************************************************\
 
-Module: Zero Initialization
+Module: Expression Initialization
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 /// \file
-/// Zero Initialization
+/// Expression Initialization
 
-#include "zero_initializer.h"
+#include "expr_initializer.h"
 
 #include "arith_tools.h"
 #include "c_types.h"
@@ -20,10 +20,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "pointer_offset_size.h"
 #include "std_expr.h"
 
-class zero_initializert:public messaget
+class expr_initializert : public messaget
 {
 public:
-  zero_initializert(
+  expr_initializert(
     const namespacet &_ns,
     message_handlert &_message_handler):
     messaget(_message_handler),
@@ -35,18 +35,18 @@ class zero_initializert:public messaget
     const typet &type,
     const source_locationt &source_location)
   {
-    return zero_initializer_rec(type, source_location);
+    return expr_initializer_rec(type, source_location);
   }
 
 protected:
   const namespacet &ns;
 
-  exprt zero_initializer_rec(
+  exprt expr_initializer_rec(
     const typet &type,
     const source_locationt &source_location);
 };
 
-exprt zero_initializert::zero_initializer_rec(
+exprt expr_initializert::expr_initializer_rec(
   const typet &type,
   const source_locationt &source_location)
 {
@@ -86,7 +86,7 @@ exprt zero_initializert::zero_initializer_rec(
   }
   else if(type_id==ID_complex)
   {
-    exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
+    exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
     complex_exprt result(sub_zero, sub_zero, to_complex_type(type));
     result.add_source_location()=source_location;
     return result;
@@ -113,7 +113,8 @@ exprt zero_initializert::zero_initializer_rec(
     }
     else
     {
-      exprt tmpval=zero_initializer_rec(array_type.subtype(), source_location);
+      exprt tmpval =
+        expr_initializer_rec(array_type.subtype(), source_location);
 
       mp_integer array_size;
 
@@ -148,7 +149,7 @@ exprt zero_initializert::zero_initializer_rec(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    exprt tmpval=zero_initializer_rec(vector_type.subtype(), source_location);
+    exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
 
     mp_integer vector_size;
 
@@ -195,7 +196,7 @@ exprt zero_initializert::zero_initializer_rec(
       }
       else
         value.copy_to_operands(
-          zero_initializer_rec(it->type(), source_location));
+          expr_initializer_rec(it->type(), source_location));
     }
 
     value.add_source_location()=source_location;
@@ -245,14 +246,14 @@ exprt zero_initializert::zero_initializer_rec(
     {
       value.set_component_name(component.get_name());
       value.op()=
-        zero_initializer_rec(component.type(), source_location);
+        expr_initializer_rec(component.type(), source_location);
     }
 
     return value;
   }
   else if(type_id==ID_symbol)
   {
-    exprt result=zero_initializer_rec(ns.follow(type), source_location);
+    exprt result = expr_initializer_rec(ns.follow(type), source_location);
     // we might have mangled the type for arrays, so keep that
     if(ns.follow(type).id()!=ID_array)
       result.type()=type;
@@ -262,21 +263,21 @@ exprt zero_initializert::zero_initializer_rec(
   else if(type_id==ID_c_enum_tag)
   {
     return
-      zero_initializer_rec(
+      expr_initializer_rec(
         ns.follow_tag(to_c_enum_tag_type(type)),
         source_location);
   }
   else if(type_id==ID_struct_tag)
   {
     return
-      zero_initializer_rec(
+      expr_initializer_rec(
         ns.follow_tag(to_struct_tag_type(type)),
         source_location);
   }
   else if(type_id==ID_union_tag)
   {
     return
-      zero_initializer_rec(
+      expr_initializer_rec(
         ns.follow_tag(to_union_tag_type(type)),
         source_location);
   }
@@ -298,7 +299,7 @@ exprt zero_initializer(
   const namespacet &ns,
   message_handlert &message_handler)
 {
-  zero_initializert z_i(ns, message_handler);
+  expr_initializert z_i(ns, message_handler);
   return z_i(type, source_location);
 }
 
@@ -312,7 +313,7 @@ exprt zero_initializer(
 
   try
   {
-    zero_initializert z_i(ns, mh);
+    expr_initializert z_i(ns, mh);
     return z_i(type, source_location);
   }
   catch(int)
diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h
@@ -1,16 +1,16 @@
 /*******************************************************************\
 
-Module: Zero Initialization
+Module: Expression Initialization
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 /// \file
-/// Zero Initialization
+/// Expression Initialization
 
-#ifndef CPROVER_UTIL_ZERO_INITIALIZER_H
-#define CPROVER_UTIL_ZERO_INITIALIZER_H
+#ifndef CPROVER_UTIL_EXPR_INITIALIZER_H
+#define CPROVER_UTIL_EXPR_INITIALIZER_H
 
 #include "expr.h"
 
@@ -30,4 +30,4 @@ exprt zero_initializer(
   const source_locationt &,
   const namespacet &);
 
-#endif // CPROVER_UTIL_ZERO_INITIALIZER_H
+#endif // CPROVER_UTIL_EXPR_INITIALIZER_H
