Merge pull request #2219 from tautschnig/nondet-initializer

kroening · web-flow · commit 10a468514c5b · 2018-06-07T09:40:57.000+01:00
nondet_initializer to build deep non-deterministic expressions
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -21,12 +21,11 @@ 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/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
-
-#include <linking/zero_initializer.h>
 #include <util/suffix.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,6 +24,7 @@ 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>
@@ -32,8 +33,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
-#include <linking/zero_initializer.h>
-
 #include <goto-programs/cfg.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/resolve_inherited_component.h>
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
@@ -12,10 +12,9 @@ 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 <linking/zero_initializer.h>
-
 #include "java_pointer_casts.h"
 #include "java_types.h"
 #include "java_utils.h"
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -8,15 +8,14 @@ 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 <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,9 +11,8 @@ 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/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/unicode.h>
 
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -14,11 +14,10 @@ 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/expr_initializer.h>
 #include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_typecheck_base.h"
 
 #include <util/config.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,14 +14,13 @@ 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 <linking/zero_initializer.h>
-
 #include "anonymous_member.h"
 
 void c_typecheck_baset::do_initializer(
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
@@ -14,10 +14,10 @@ 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 <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
@@ -19,12 +19,11 @@ 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 <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
@@ -13,10 +13,9 @@ 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 <linking/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,14 +14,14 @@ 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 <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
@@ -16,12 +16,11 @@ 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 <linking/zero_initializer.h>
-
 #include <langapi/language_util.h>
 
 #include "format_strings.h"
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
@@ -13,13 +13,12 @@ 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 <linking/zero_initializer.h>
-
 inline static typet c_sizeof_type_rec(const exprt &expr)
 {
   const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
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/expr_initializer.h>
 
 void goto_symext::symex_start_thread(statet &state)
 {
diff --git a/src/linking/CMakeLists.txt b/src/linking/CMakeLists.txt
@@ -3,4 +3,4 @@ add_library(linking ${sources})
 
 generic_includes(linking)
 
-target_link_libraries(linking util ansi-c)
+target_link_libraries(linking util)
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/module_dependencies.txt b/src/linking/module_dependencies.txt
@@ -1,4 +1,3 @@
-ansi-c # should go away
 goto-programs
 langapi # should go away
 linking
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/expr_initializer.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 <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
@@ -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 \
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h
