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.
diffblue · Mar 27, 2024 · 40b2f25 · 40b2f25
1 parent 08b2f2f
commit 40b2f25
Show file tree

Hide file tree

Showing 98 changed files with 1,412 additions and 1,457 deletions.
diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -16,10 +16,11 @@ Author: Diffblue Ltd.
 #include <util/symbol_table_base.h>
 #include <util/unicode.h>
 
-#include <goto-programs/allocate_objects.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_instruction_code.h>
 
+#include <ansi-c/allocate_objects.h>
+
 #include "ci_lazy_methods_needed.h"
 #include "code_with_references.h"
 #include "java_static_initializers.h"

diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/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"

diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/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;

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/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"
 

diff --git a/jbmc/src/java_bytecode/lazy_goto_functions_map.h b/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

diff --git a/jbmc/src/java_bytecode/nondet.cpp b/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,

diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/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"
 

diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/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>

diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt
@@ -1,3 +1,4 @@
+ansi-c
 testing-utils
 java-testing-utils
 analyses

diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/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)

diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt b/jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt
@@ -1,3 +1,4 @@
+ansi-c
 goto-programs
 java_bytecode
 java-testing-utils

diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/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)

diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/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,

diff --git a/jbmc/unit/java_bytecode/module_dependencies.txt b/jbmc/unit/java_bytecode/module_dependencies.txt
@@ -1,3 +1,4 @@
+ansi-c
 java_bytecode
 linking
 testing-utils

diff --git a/src/ansi-c/Makefile b/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 \

diff --git a/src/goto-programs/allocate_objects.cpp → src/ansi-c/allocate_objects.cpp b/src/goto-programs/allocate_objects.cpp → 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

diff --git a/src/goto-programs/allocate_objects.h → src/ansi-c/allocate_objects.h b/src/goto-programs/allocate_objects.h → 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>

diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.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.

diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
@@ -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;