Move unwindset.{h,cpp} to goto-programs

tautschnig · tautschnig · commit 059fe90cb960 · 2025-05-28T11:11:50.000Z
This code is not specific to goto-instrument and used more widely across
the code base. Removes a now-unnecessary dependency of goto-checker on
goto-instrument.
diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
@@ -32,7 +32,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
       ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
       ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
       ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
@@ -116,7 +116,6 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
-              $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
               $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
               $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -36,7 +36,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
-      ../goto-instrument/unwindset$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
diff --git a/src/goto-checker/CMakeLists.txt b/src/goto-checker/CMakeLists.txt
@@ -3,4 +3,4 @@ add_library(goto-checker ${sources})
 
 generic_includes(goto-checker)
 
-target_link_libraries(goto-checker goto-programs goto-symex solvers util xml goto-instrument-lib)
+target_link_libraries(goto-checker goto-programs goto-symex solvers util xml)
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
@@ -12,7 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
 #define CPROVER_GOTO_CHECKER_BMC_UTIL_H
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
 #include <goto-symex/build_goto_trace.h>
 
 #include "incremental_goto_checker.h"
diff --git a/src/goto-checker/module_dependencies.txt b/src/goto-checker/module_dependencies.txt
@@ -1,7 +1,6 @@
 assembler
 cbmc # symex_bmc will be moved next
 goto-checker
-goto-instrument
 goto-programs
 goto-symex
 langapi
diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h
@@ -12,12 +12,11 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
 #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
 
-#include "incremental_goto_checker.h"
+#include <goto-programs/unwindset.h>
 
 #include <goto-symex/path_storage.h>
 
-#include <goto-instrument/unwindset.h>
-
+#include "incremental_goto_checker.h"
 #include "symex_bmc.h"
 
 class multi_path_symex_only_checkert : public incremental_goto_checkert
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.h b/src/goto-checker/single_loop_incremental_symex_checker.h
@@ -14,9 +14,9 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
 
-#include <goto-symex/path_storage.h>
+#include <goto-programs/unwindset.h>
 
-#include <goto-instrument/unwindset.h>
+#include <goto-symex/path_storage.h>
 
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h
@@ -12,7 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 #define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
 #include <goto-symex/path_storage.h>
 
 #include "incremental_goto_checker.h"
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
@@ -11,12 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_bmc.h"
 
-#include <limits>
-
 #include <util/simplify_expr.h>
 #include <util/source_location.h>
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
+#include <limits>
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp
@@ -6,13 +6,13 @@ Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <limits>
-
 #include "symex_bmc_incremental_one_loop.h"
 
 #include <util/structured_data.h>
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
+#include <limits>
 
 symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   message_handlert &message_handler,
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
@@ -99,7 +99,6 @@ SRC = accelerate/accelerate.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \
       unwind.cpp \
-      unwindset.cpp \
       value_set_fi_fp_removal.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -27,13 +27,13 @@ Date: February 2016
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/goto_program.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/unwindset.h>
 
 #include <analyses/local_may_alias.h>
 #include <ansi-c/c_expr.h>
 #include <goto-instrument/havoc_utils.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/unwind.h>
-#include <goto-instrument/unwindset.h>
 #include <langapi/language_util.h>
 
 #include "cfg_info.h"
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
@@ -20,13 +20,13 @@ Author: Remi Delmas, delmarsd@amazon.com
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/c_expr.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/unwind.h>
-#include <goto-instrument/unwindset.h>
 #include <langapi/language_util.h>
 
 #include "dfcc_cfg_info.h"
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -20,14 +20,14 @@ Author: Remi Delmas, delmarsd@amazon.com
 
 #include <goto-programs/goto_function.h>
 #include <goto-programs/goto_model.h>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/c_expr.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
 #include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/unwind.h>
-#include <goto-instrument/unwindset.h>
 #include <linking/static_lifetime_init.h>
 
 #include "dfcc_utils.h"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/restrict_function_pointers.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/goto-conversion/goto_check_c.h>
@@ -39,7 +40,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "reachability_slicer.h"
 #include "replace_calls.h"
 #include "uninitialized.h"
-#include "unwindset.h"
 
 #include "contracts/contracts.h"
 #include "contracts/contracts_wrangler.h"
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
@@ -20,8 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 
 #include <goto-programs/goto_functions.h>
-
-#include "unwindset.h"
+#include <goto-programs/unwindset.h>
 
 void goto_unwindt::copy_segment(
   const goto_programt::const_targett start,
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
@@ -56,6 +56,7 @@ SRC = adjust_float_expressions.cpp \
       string_abstraction.cpp \
       structured_trace_util.cpp \
       system_library_symbols.cpp \
+      unwindset.cpp \
       validate_code.cpp \
       validate_goto_model.cpp \
       vcd_goto_trace.cpp \
diff --git a/src/goto-programs/unwindset.cpp b/src/goto-programs/unwindset.cpp
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol_table.h>
 #include <util/unicode.h>
 
-#include <goto-programs/abstract_goto_model.h>
+#include "abstract_goto_model.h"
 
 #include <algorithm>
 #include <fstream>
@@ -216,7 +216,7 @@ void unwindsett::parse_unwindset_file(
   std::ifstream file(widen_if_needed(file_name));
 
   if(!file)
-    throw "cannot open file "+file_name;
+    throw "cannot open file " + file_name;
 
   std::stringstream buffer;
   buffer << file.rdbuf();
diff --git a/src/goto-programs/unwindset.h b/src/goto-programs/unwindset.h
diff --git a/src/goto-synthesizer/Makefile b/src/goto-synthesizer/Makefile
@@ -26,7 +26,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/loop_utils$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/unwind$(OBJEXT) \
-      ../goto-instrument/unwindset$(OBJEXT) \
       ../goto-symex/goto-symex$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
diff --git a/src/libcprover-cpp/Makefile b/src/libcprover-cpp/Makefile
@@ -25,7 +25,6 @@ OBJ += \
   ../goto-instrument/nondet_static$(OBJEXT) \
   ../goto-instrument/reachability_slicer$(OBJEXT) \
   ../goto-instrument/source_lines$(OBJEXT) \
-  ../goto-instrument/unwindset$(OBJEXT) \
   ../goto-programs/goto-programs$(LIBEXT) \
   ../goto-symex/goto-symex$(LIBEXT) \
   ../json-symtab-language/json-symtab-language$(LIBEXT) \
diff --git a/unit/Makefile b/unit/Makefile
@@ -260,7 +260,6 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/goto-instrument/reachability_slicer$(OBJEXT) \
           ../src/goto-instrument/nondet_static$(OBJEXT) \
           ../src/goto-instrument/full_slicer$(OBJEXT) \
-          ../src/goto-instrument/unwindset$(OBJEXT) \
           ../src/goto-synthesizer/expr_enumerator$(OBJEXT) \
           ../src/xmllang/xmllang$(LIBEXT) \
           ../src/goto-symex/goto-symex$(LIBEXT) \
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
@@ -6,31 +6,25 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2018
 
 \*******************************************************************/
 
-#include <testing-utils/use_catch.h>
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/tempfile.h>
 
-#include <path_strategies.h>
-
-#include <fstream>
-#include <functional>
-#include <string>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/ansi_c_language.h>
-
 #include <cbmc/cbmc_parse_options.h>
-
 #include <goto-checker/bmc_util.h>
 #include <goto-checker/goto_symex_property_decider.h>
 #include <goto-checker/symex_bmc.h>
-
 #include <goto-symex/path_storage.h>
-
-#include <goto-instrument/unwindset.h>
-
 #include <langapi/mode.h>
+#include <testing-utils/use_catch.h>
 
-#include <util/cmdline.h>
-#include <util/config.h>
-#include <util/tempfile.h>
+#include <fstream>
+#include <functional>
+#include <path_strategies.h>
+#include <string>
 
 // The actual test suite.
 //

Original file line number	Diff line number	Diff line change
`@@ -3,4 +3,4 @@ add_library(goto-checker ${sources})`
`3`	`3`
`4`	`4`	`generic_includes(goto-checker)`
`5`	`5`
`6`		`-target_link_libraries(goto-checker goto-programs goto-symex solvers util xml goto-instrument-lib)`
	`6`	`+target_link_libraries(goto-checker goto-programs goto-symex solvers util xml)`