Move adjust_float_expressions to goto-programs

Author: hannes-steffenhagen-diffblue

src/cbmc/cbmc_parse_options.cpp

@@ -26,6 +26,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_preprocess.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/convert_nondet.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
@@ -49,7 +51,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_instrumentation.h>
 
 #include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>

src/clobber/Makefile

@@ -13,7 +13,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../assembler/assembler$(LIBEXT) \
        ../solvers/solvers$(LIBEXT) \
        ../util/util$(LIBEXT) \
-       ../goto-symex/adjust_float_expressions$(OBJEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/dump_c$(OBJEXT) \

src/goto-diff/Makefile

@@ -25,7 +25,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../goto-instrument/cover_instrument_other$(OBJEXT) \
       ../goto-instrument/cover_util$(OBJEXT) \
-      ../goto-symex/adjust_float_expressions$(OBJEXT) \
       ../goto-symex/rewrite_union$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \

src/goto-diff/goto_diff_parse_options.cpp

@@ -24,6 +24,7 @@ Author: Peter Schrammel
 
 #include <langapi/language.h>
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/mm_io.h>
@@ -45,7 +46,6 @@ Author: Peter Schrammel
 #include <goto-programs/link_to_library.h>
 
 #include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/cover.h>
 

src/goto-programs/Makefile

@@ -1,4 +1,5 @@
-SRC = basic_blocks.cpp \
+SRC = adjust_float_expressions.cpp \
+      basic_blocks.cpp \
       builtin_functions.cpp \
       class_hierarchy.cpp \
       class_identifier.cpp \

src/goto-symex/adjust_float_expressions.cpp renamed to src/goto-programs/adjust_float_expressions.cpp

@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 #include <util/arith_tools.h>
 
-#include <goto-programs/goto_model.h>
+#include "goto_model.h"
 
 static bool have_to_adjust_float_expressions(
   const exprt &expr,

src/goto-symex/adjust_float_expressions.h renamed to src/goto-programs/adjust_float_expressions.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution
 
-#ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
-#define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
+#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
+#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
 
 #include <goto-programs/goto_functions.h>
 
@@ -31,4 +31,4 @@ void adjust_float_expressions(
   const namespacet &ns);
 void adjust_float_expressions(goto_modelt &goto_model);
 
-#endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
+#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H

src/goto-symex/Makefile

@@ -1,5 +1,4 @@
-SRC = adjust_float_expressions.cpp \
-      auto_objects.cpp \
+SRC = auto_objects.cpp \
       build_goto_trace.cpp \
       goto_symex.cpp \
       goto_symex_state.cpp \

src/jbmc/jbmc_parse_options.cpp

@@ -26,6 +26,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_language.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/convert_nondet.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
@@ -41,8 +43,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
 
-#include <goto-symex/adjust_float_expressions.h>
-
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>