From ed3e01dbd1b507da6b0f1f6c5dd4b89d2144d5cd Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 16 May 2018 11:38:02 +0100
Subject: [PATCH] Move convert_nondet to java_bytecode

---
 src/cbmc/cbmc_parse_options.cpp                       |  1 -
 src/goto-programs/Makefile                            |  1 -
 src/java_bytecode/Makefile                            |  1 +
 .../convert_nondet.cpp                                | 11 ++++++-----
 src/{goto-programs => java_bytecode}/convert_nondet.h |  6 +++---
 src/jbmc/jbmc_parse_options.cpp                       |  2 +-
 6 files changed, 11 insertions(+), 11 deletions(-)
 rename src/{goto-programs => java_bytecode}/convert_nondet.cpp (96%)
 rename src/{goto-programs => java_bytecode}/convert_nondet.h (91%)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 295efe9c38f3..bedc9ae667dc 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -26,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/c_preprocess.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>
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index cefd43949cef..c90d750b1d9e 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -3,7 +3,6 @@ SRC = basic_blocks.cpp \
       class_hierarchy.cpp \
       class_identifier.cpp \
       compute_called_functions.cpp \
-      convert_nondet.cpp \
       destructor.cpp \
       elf_reader.cpp \
       format_strings.cpp \
diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile
index d0071f969124..f399ba0d4ed1 100644
--- a/src/java_bytecode/Makefile
+++ b/src/java_bytecode/Makefile
@@ -2,6 +2,7 @@ SRC = bytecode_info.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       ci_lazy_methods_needed.cpp \
+      convert_nondet.cpp \
       expr2java.cpp \
       generic_parameter_specialization_map_keys.cpp \
       jar_file.cpp \
diff --git a/src/goto-programs/convert_nondet.cpp b/src/java_bytecode/convert_nondet.cpp
similarity index 96%
rename from src/goto-programs/convert_nondet.cpp
rename to src/java_bytecode/convert_nondet.cpp
index 79620c97a5f5..6a1c5c4b0926 100644
--- a/src/goto-programs/convert_nondet.cpp
+++ b/src/java_bytecode/convert_nondet.cpp
@@ -10,17 +10,18 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 /// Convert side_effect_expr_nondett expressions
 
 #include "convert_nondet.h"
-#include "goto_convert.h"
-#include "goto_model.h"
-#include "remove_skip.h"
 
-#include <java_bytecode/java_object_factory.h> // gen_nondet_init
+#include <goto-programs/goto_convert.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_skip.h>
 
-#include <util/irep_ids.h>
 #include <util/fresh_symbol.h>
+#include <util/irep_ids.h>
 
 #include <memory>
 
+#include "java_object_factory.h" // gen_nondet_init
+
 /// Checks an instruction to see whether it contains an assignment from
 /// side_effect_expr_nondet.  If so, replaces the instruction with a range of
 /// instructions to properly nondet-initialize the lhs.
diff --git a/src/goto-programs/convert_nondet.h b/src/java_bytecode/convert_nondet.h
similarity index 91%
rename from src/goto-programs/convert_nondet.h
rename to src/java_bytecode/convert_nondet.h
index 7bd3c2ce3ce6..8edbcc266276 100644
--- a/src/goto-programs/convert_nondet.h
+++ b/src/java_bytecode/convert_nondet.h
@@ -9,8 +9,8 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 /// \file
 /// Convert side_effect_expr_nondett expressions
 
-#ifndef CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H
-#define CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H
+#ifndef CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
+#define CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 
 #include <cstddef> // size_t
 #include <util/irep.h>
@@ -52,4 +52,4 @@ void convert_nondet(
   const object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode);
 
-#endif
+#endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index fd4614670604..8067e31ff9b6 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -26,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/ansi_c_language.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>
@@ -54,6 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
+#include <java_bytecode/convert_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
 #include <java_bytecode/remove_exceptions.h>