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

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,10 @@ SRC = anonymous_member.cpp \
       ansi_c_typecheck.cpp \
       ansi_c_y.tab.cpp \
       builtin_factory.cpp \
+      builtin_functions.cpp \
+      format_strings.cpp \
+      printf_formatter.cpp \
+      string_instrumentation.cpp \
       c_expr.cpp \
       c_misc.cpp \
       c_nondet_symbol_factory.cpp \
@@ -32,7 +37,17 @@ SRC = anonymous_member.cpp \
       expr2c.cpp \
       gcc_types.cpp \
       gcc_version.cpp \
+      goto_asm.cpp \
+      destructor.cpp \
+      goto_convert.cpp \
       goto_check_c.cpp \
+      goto_convert_exceptions.cpp \
+      goto_clean_expr.cpp \
+      goto_convert_functions.cpp \
+      goto_convert_function_call.cpp \
+      goto_convert_side_effect.cpp \
+      link_to_library.cpp \
+      scope_tree.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

@@ -6,8 +6,8 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
-#define CPROVER_UTIL_ALLOCATE_OBJECTS_H
+#ifndef CPROVER_ANSI_C_ALLOCATE_OBJECTS_H
+#define CPROVER_ANSI_C_ALLOCATE_OBJECTS_H
 
 #include <util/namespace.h>
 #include <util/std_code.h>

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

@@ -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

@@ -14,7 +14,7 @@ Author: Diffblue Ltd.
 
 #include <set>
 
-#include <goto-programs/allocate_objects.h>
+#include "allocate_objects.h"
 
 struct c_object_factory_parameterst;
 

src/ansi-c/c_nondet_symbol_factory.h

@@ -10,7 +10,7 @@ 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/destructor.cpp renamed to src/ansi-c/destructor.cpp

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Destructor Calls
 
-#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
-#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
+#ifndef CPROVER_ANSI_C_DESTRUCTOR_H
+#define CPROVER_ANSI_C_DESTRUCTOR_H
 
 class namespacet;
 class typet;

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

@@ -9,8 +9,8 @@ Author: CM Wintersteiger
 /// \file
 /// Format String Parser
 
-#ifndef CPROVER_GOTO_PROGRAMS_FORMAT_STRINGS_H
-#define CPROVER_GOTO_PROGRAMS_FORMAT_STRINGS_H
+#ifndef CPROVER_ANSI_C_FORMAT_STRINGS_H
+#define CPROVER_ANSI_C_FORMAT_STRINGS_H
 
 #include <util/irep.h>
 #include <util/mp_arith.h>

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

@@ -25,7 +25,7 @@ Author: Daniel Kroening, [email protected]
 #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/format_strings.h renamed to src/ansi-c/format_strings.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Program Transformation
 
-#ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_H
-#define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_H
+#ifndef CPROVER_ANSI_C_GOTO_CONVERT_H
+#define CPROVER_ANSI_C_GOTO_CONVERT_H
 
 #include <util/irep.h>
 

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

@@ -9,16 +9,17 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Program Transformation
 
-#ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
-#define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
+#ifndef CPROVER_ANSI_C_GOTO_CONVERT_CLASS_H
+#define CPROVER_ANSI_C_GOTO_CONVERT_CLASS_H
 
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_expr.h>
 #include <util/std_code.h>
 
+#include <goto-programs/goto_program.h>
+
 #include "allocate_objects.h"
-#include "goto_program.h"
 #include "scope_tree.h"
 
 #include <list>

src/goto-programs/goto_clean_expr.cpp renamed to src/ansi-c/goto_clean_expr.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/goto_convert.cpp renamed to src/ansi-c/goto_convert.cpp

@@ -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_convert.h renamed to src/ansi-c/goto_convert.h

@@ -13,10 +13,10 @@ 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_convert_functions.h"
-#include "goto_model.h"
-#include "link_goto_model.h"
+#include <goto-programs/goto_model.h>
+#include <goto-programs/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/goto-programs/goto_convert_class.h renamed to src/ansi-c/goto_convert_class.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Library Linking
 
-#ifndef CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
-#define CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
+#ifndef CPROVER_ANSI_C_LINK_TO_LIBRARY_H
+#define CPROVER_ANSI_C_LINK_TO_LIBRARY_H
 
 #include <functional>
 #include <set>

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

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// printf Formatting
 
-#ifndef CPROVER_GOTO_PROGRAMS_PRINTF_FORMATTER_H
-#define CPROVER_GOTO_PROGRAMS_PRINTF_FORMATTER_H
+#ifndef CPROVER_ANSI_C_PRINTF_FORMATTER_H
+#define CPROVER_ANSI_C_PRINTF_FORMATTER_H
 
 #include <util/expr.h>
 

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

@@ -6,8 +6,8 @@
 
 \*******************************************************************/
 
-#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
-#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
+#ifndef CPROVER_ANSI_C_DESTRUCTOR_TREE_H
+#define CPROVER_ANSI_C_DESTRUCTOR_TREE_H
 
 #include <util/graph.h>
 #include <util/std_code_base.h>

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

@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/string_constant.h>
 
-#include <goto-programs/format_strings.h>
+#include "format_strings.h"
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 

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

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// String Abstraction
 
-#ifndef CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
-#define CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
+#ifndef CPROVER_ANSI_C_STRING_INSTRUMENTATION_H
+#define CPROVER_ANSI_C_STRING_INSTRUMENTATION_H
 
 class exprt;
 class goto_functionst;

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

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/version.h>
 
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/link_to_library.h>
+#include <ansi-c/link_to_library.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>

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

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/version.h>
 
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/link_to_library.h>
+#include <ansi-c/link_to_library.h>
 #include <goto-programs/process_goto_program.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>

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

@@ -23,7 +23,7 @@ Date: June 2006
 #include <util/unicode.h>
 #include <util/version.h>
 
-#include <goto-programs/goto_convert_functions.h>
+#include <ansi-c/goto_convert_functions.h>
 #include <goto-programs/name_mangler.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/write_goto_binary.h>

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

@@ -17,7 +17,8 @@ Author: Kareem Khazem <[email protected]>, 2017
 #include <util/run.h>
 #include <util/tempfile.h>
 
-#include <goto-programs/goto_convert_functions.h>
+#include <ansi-c/goto_convert_functions.h>
+
 #include <goto-programs/goto_model.h>
 #include <goto-programs/read_goto_binary.h>
 

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

@@ -18,7 +18,7 @@ Author: Peter Schrammel
 #include <util/version.h>
 
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/link_to_library.h>
+#include <ansi-c/link_to_library.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/process_goto_program.h>
 #include <goto-programs/remove_skip.h>

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

@@ -16,8 +16,8 @@ Author: Diffblue Ltd.
 #include <util/string_utils.h>
 #include <util/ui_message.h>
 
-#include <goto-programs/allocate_objects.h>
-#include <goto-programs/goto_convert_functions.h>
+#include <ansi-c/allocate_objects.h>
+#include <ansi-c/goto_convert_functions.h>
 #include <goto-programs/goto_model.h>
 
 #include "function_harness_generator_options.h"

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

@@ -16,7 +16,7 @@ Author: Daniel Poetzl
 #include <util/string_utils.h>
 #include <util/symbol_table.h>
 
-#include <goto-programs/goto_convert_functions.h>
+#include <ansi-c/goto_convert_functions.h>
 #include <goto-programs/goto_model.h>
 
 #include <json-symtab-language/json_symbol_table.h>

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

@@ -15,7 +15,7 @@ Date: June 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H
 
-#include <goto-programs/goto_convert_class.h>
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/byte_operators.h>
 #include <util/expr_cast.h>

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

@@ -14,7 +14,7 @@ Date: February 2016
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
 
-#include <goto-programs/goto_convert_class.h>
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/message.h>
 #include <util/namespace.h>

src/cbmc/cbmc_parse_options.cpp

@@ -23,12 +23,13 @@ Author: Remi Delmas, [email protected]
 #include <util/std_expr.h>
 #include <util/string_utils.h>
 
-#include <goto-programs/goto_convert_functions.h>
+#include <ansi-c/goto_convert_functions.h>
+
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/goto_model.h>
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/link_to_library.h>
+#include <ansi-c/link_to_library.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -14,7 +14,7 @@ Date: February 2023
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
 
-#include <goto-programs/goto_convert_class.h>
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/message.h>
 #include <util/namespace.h>

src/goto-cc/compile.cpp

@@ -14,7 +14,7 @@ Date: August 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
 
-#include <goto-programs/goto_convert_class.h>
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/message.h>
 #include <util/namespace.h>

src/goto-cc/linker_script_merge.cpp

@@ -13,7 +13,7 @@ Date: August 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H
 
-#include <goto-programs/goto_convert_class.h>
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/message.h>
 #include <util/namespace.h>

src/goto-diff/goto_diff_parse_options.cpp

@@ -11,7 +11,8 @@ Date: April 2023
 \*******************************************************************/
 
 #include "dfcc_instrument_loop.h"
-#include <goto-programs/goto_convert_class.h>
+
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/format_expr.h>
 #include <util/fresh_symbol.h>

src/goto-harness/function_call_harness_generator.cpp

@@ -18,7 +18,7 @@ Author: Remi Delmas, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-#include <goto-programs/goto_convert_functions.h>
+#include <ansi-c/goto_convert_functions.h>
 #include <goto-programs/goto_function.h>
 #include <goto-programs/goto_model.h>
 

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -7,7 +7,8 @@ Author: Remi Delmas, [email protected]
 \*******************************************************************/
 
 #include "dfcc_spec_functions.h"
-#include <goto-programs/goto_convert_class.h>
+
+#include <ansi-c/goto_convert_class.h>
 
 #include <util/format_expr.h>
 #include <util/namespace.h>