move goto_convert from goto-programs/ to ansi-c/

The goto_convertt class and associated helpers convert a C parse tree into a
set of GOTO functions.  They are specific to C, and hence, should be in the
ansi-c/ directory.

Author: kroening

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -16,7 +16,8 @@ Author: Diffblue Ltd.
 #include <util/symbol_table_base.h>
 #include <util/unicode.h>
 
-#include <goto-programs/allocate_objects.h>
+#include <ansi-c/allocate_objects.h>
+
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_instruction_code.h>
 

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -11,10 +11,11 @@ Author: Reuben Thomas, [email protected]
 
 #include "convert_java_nondet.h"
 
-#include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
+#include <ansi-c/goto-conversion/goto_convert.h>
+
 #include "java_object_factory.h" // gen_nondet_init
 #include "java_object_factory_parameters.h"
 #include "java_utils.h"

jbmc/src/java_bytecode/java_object_factory.h

@@ -71,11 +71,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 
-#include "nondet.h"
+#include <util/std_code.h>
 
-#include <goto-programs/allocate_objects.h>
+#include <ansi-c/allocate_objects.h>
 
-#include <util/std_code.h>
+#include "nondet.h"
 
 class message_handlert;
 class select_pointer_typet;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -29,9 +29,10 @@ Date:   April 2017
 #include <util/string_expr.h>
 #include <util/symbol_table_base.h>
 
-#include <goto-programs/allocate_objects.h>
 #include <goto-programs/class_identifier.h>
 
+#include <ansi-c/allocate_objects.h>
+
 #include "java_types.h"
 #include "java_utils.h"
 

jbmc/src/java_bytecode/lazy_goto_functions_map.h

@@ -6,15 +6,16 @@
 #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
 #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
 
-#include <unordered_set>
+#include <util/journalling_symbol_table.h>
+#include <util/message.h>
+#include <util/symbol_table_builder.h>
 
-#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_functions.h>
 
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <langapi/language_file.h>
-#include <util/journalling_symbol_table.h>
-#include <util/message.h>
-#include <util/symbol_table_builder.h>
+
+#include <unordered_set>
 
 /// Provides a wrapper for a map of lazily loaded goto_functiont.
 /// This incrementally builds a goto-functions object, while permitting

jbmc/src/java_bytecode/nondet.cpp

@@ -8,10 +8,10 @@ Author: Diffblue Ltd.
 
 #include "nondet.h"
 
-#include <goto-programs/allocate_objects.h>
-
 #include <util/arith_tools.h>
 
+#include <ansi-c/allocate_objects.h>
+
 symbol_exprt generate_nondet_int(
   const exprt &min_value_expr,
   const exprt &max_value_expr,

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -19,9 +19,10 @@ Author: Peter Schrammel
 #include <util/std_code.h>
 
 #include <goto-programs/class_identifier.h>
-#include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_model.h>
 
+#include <ansi-c/goto-conversion/goto_convert.h>
+
 #include "java_types.h"
 #include "java_utils.h"
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_check.h>
-#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/remove_returns.h>
@@ -33,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_symbol_table.h>
 
 #include <ansi-c/ansi_c_language.h>
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>

jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt

@@ -1,3 +1,4 @@
+ansi-c
 testing-utils
 java-testing-utils
 analyses

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -8,13 +8,14 @@ Author: Diffblue Limited.
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/message.h>
-#include <testing-utils/use_catch.h>
 
-#include <analyses/local_safe_pointers.h>
-#include <goto-programs/goto_convert_functions.h>
 #include <util/expr_iterator.h>
 
+#include <analyses/local_safe_pointers.h>
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
 // We're expecting a call "something->field . B.virtualmethod()":
 static bool is_expected_virtualmethod_call(
   const goto_programt::instructiont &instruction)

jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt

@@ -1,3 +1,4 @@
+ansi-c
 goto-programs
 java_bytecode
 java-testing-utils

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -8,18 +8,18 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/message.h>
-#include <testing-utils/use_catch.h>
 
 #include <goto-programs/class_hierarchy.h>
-#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_virtual_functions.h>
 
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_object_factory_parameters.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/replace_java_nondet.h>
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 void validate_nondet_method_removed(
   std::list<goto_programt::instructiont> instructions)

jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt

@@ -1,3 +1,4 @@
+ansi-c/goto-conversion
 goto-instrument
 goto-programs
 java_bytecode

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -7,15 +7,17 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/message.h>
-#include <testing-utils/use_catch.h>
 
-#include <goto-programs/goto_convert_functions.h>
-#include <goto-programs/remove_virtual_functions.h>
 #include <util/config.h>
-#include <goto-instrument/cover.h>
 #include <util/options.h>
 
+#include <goto-programs/remove_virtual_functions.h>
+
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
+#include <goto-instrument/cover.h>
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
 void check_function_call(
   const equal_exprt &eq_expr,
   const irep_idt &class_name,

jbmc/unit/java_bytecode/module_dependencies.txt

@@ -1,3 +1,4 @@
+ansi-c
 java_bytecode
 linking
 testing-utils

src/ansi-c/Makefile

@@ -1,4 +1,5 @@
-SRC = anonymous_member.cpp \
+SRC = allocate_objects.cpp \
+      anonymous_member.cpp \
       ansi_c_convert_type.cpp \
       ansi_c_declaration.cpp \
       ansi_c_entry_point.cpp \
@@ -11,6 +12,7 @@ SRC = anonymous_member.cpp \
       ansi_c_typecheck.cpp \
       ansi_c_y.tab.cpp \
       builtin_factory.cpp \
+      printf_formatter.cpp \
       c_expr.cpp \
       c_misc.cpp \
       c_nondet_symbol_factory.cpp \
@@ -32,7 +34,20 @@ SRC = anonymous_member.cpp \
       expr2c.cpp \
       gcc_types.cpp \
       gcc_version.cpp \
-      goto_check_c.cpp \
+      goto-conversion/builtin_functions.cpp \
+      goto-conversion/goto_asm.cpp \
+      goto-conversion/destructor.cpp \
+      goto-conversion/format_strings.cpp \
+      goto-conversion/goto_convert.cpp \
+      goto-conversion/goto_check_c.cpp \
+      goto-conversion/goto_convert_exceptions.cpp \
+      goto-conversion/goto_clean_expr.cpp \
+      goto-conversion/goto_convert_functions.cpp \
+      goto-conversion/goto_convert_function_call.cpp \
+      goto-conversion/goto_convert_side_effect.cpp \
+      goto-conversion/link_to_library.cpp \
+      goto-conversion/scope_tree.cpp \
+      goto-conversion/string_instrumentation.cpp \
       literals/convert_character_literal.cpp \
       literals/convert_float_literal.cpp \
       literals/convert_integer_literal.cpp \

src/goto-programs/allocate_objects.cpp renamed to src/ansi-c/allocate_objects.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/symbol.h>
 
-#include "goto_instruction_code.h"
+#include <goto-programs/goto_instruction_code.h>
 
 /// Allocates a new object, either by creating a local variable with automatic
 /// lifetime, a global variable with static lifetime, or by dynamically

src/goto-programs/allocate_objects.h renamed to src/ansi-c/allocate_objects.h

@@ -20,10 +20,10 @@ Author: Diffblue Ltd.
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
-#include <goto-programs/allocate_objects.h>
 #include <goto-programs/goto_functions.h>
 
-#include <ansi-c/c_object_factory_parameters.h>
+#include "allocate_objects.h"
+#include "c_object_factory_parameters.h"
 
 /// Creates a nondet for expr, including calling itself recursively to make
 /// appropriate symbols to point to if expr is a pointer.

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -12,9 +12,9 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
 #define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
 
-#include <set>
+#include "allocate_objects.h"
 
-#include <goto-programs/allocate_objects.h>
+#include <set>
 
 struct c_object_factory_parameterst;
 

src/ansi-c/c_nondet_symbol_factory.h

@@ -10,7 +10,8 @@ Author: Daniel Kroening, [email protected]
 /// Destructor Calls
 
 #include "destructor.h"
-#include "goto_instruction_code.h"
+
+#include <goto-programs/goto_instruction_code.h>
 
 #include <util/namespace.h>
 #include <util/pointer_expr.h>

src/goto-programs/builtin_functions.cpp renamed to src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -39,7 +39,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
-#include "c_expr.h"
+#include <ansi-c/c_expr.h>
 
 #include <algorithm>
 

src/goto-programs/destructor.cpp renamed to src/ansi-c/goto-conversion/destructor.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Program Transformation
 
+#include "destructor.h"
 #include "goto_convert.h"
 #include "goto_convert_class.h"
 
@@ -24,8 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 #include <util/symbol_table_builder.h>
 
-#include "destructor.h"
-#include "remove_skip.h"
+#include <goto-programs/remove_skip.h>
 
 static bool is_empty(const goto_programt &goto_program)
 {

src/goto-programs/destructor.h renamed to src/ansi-c/goto-conversion/destructor.h

@@ -17,14 +17,16 @@ Author: Daniel Kroening, [email protected]
 #include <util/replace_expr.h>
 #include <util/std_code.h>
 
-#include "allocate_objects.h"
-#include "goto_program.h"
-#include "scope_tree.h"
+#include <ansi-c/allocate_objects.h>
+
+#include <goto-programs/goto_program.h>
 
 #include <list>
 #include <unordered_set>
 #include <vector>
 
+#include "scope_tree.h"
+
 class side_effect_expr_overflowt;
 struct build_declaration_hops_inputst;
 

src/goto-programs/format_strings.cpp renamed to src/ansi-c/goto-conversion/format_strings.cpp

@@ -15,7 +15,7 @@ Date: June 2003
 
 #include <linking/static_lifetime_init.h>
 
-#include "goto_model.h"
+#include <goto-programs/goto_model.h>
 
 goto_convert_functionst::goto_convert_functionst(
   symbol_table_baset &_symbol_table,

src/goto-programs/format_strings.h renamed to src/ansi-c/goto-conversion/format_strings.h

@@ -15,7 +15,8 @@ Date: June 2003
 #define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_FUNCTIONS_H
 
 #include "goto_convert_class.h"
-#include "goto_functions.h"
+
+#include <goto-programs/goto_functions.h>
 
 class goto_modelt;
 

src/goto-programs/goto_asm.cpp renamed to src/ansi-c/goto-conversion/goto_asm.cpp

@@ -13,10 +13,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/static_lifetime_init.h>
 
-#include "compute_called_functions.h"
+#include <goto-programs/compute_called_functions.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/link_goto_model.h>
+
 #include "goto_convert_functions.h"
-#include "goto_model.h"
-#include "link_goto_model.h"
 
 /// Try to add \p missing_function from \p library to \p goto_model.
 static std::pair<std::optional<replace_symbolt::expr_mapt>, bool>

src/ansi-c/goto_check_c.cpp renamed to src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -0,0 +1,4 @@
+ansi-c
+goto-programs
+linking
+util

src/ansi-c/goto_check_c.h renamed to src/ansi-c/goto-conversion/goto_check_c.h

@@ -20,10 +20,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/string_constant.h>
 
-#include <goto-programs/format_strings.h>
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
+#include "format_strings.h"
+
 exprt is_zero_string(const exprt &what, bool write)
 {
   unary_exprt result{"is_zero_string", what, c_bool_type()};