diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 295efe9c38f..bedc9ae667d 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 -#include #include #include #include diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index cefd43949ce..c90d750b1d9 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 d0071f96912..6cb0f1e84b7 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_java_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_java_nondet.cpp similarity index 96% rename from src/goto-programs/convert_nondet.cpp rename to src/java_bytecode/convert_java_nondet.cpp index 79620c97a5f..735ba4400ba 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/java_bytecode/convert_java_nondet.cpp @@ -9,18 +9,19 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com /// \file /// Convert side_effect_expr_nondett expressions -#include "convert_nondet.h" -#include "goto_convert.h" -#include "goto_model.h" -#include "remove_skip.h" +#include "convert_java_nondet.h" -#include // gen_nondet_init +#include +#include +#include -#include #include +#include #include +#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_java_nondet.h similarity index 91% rename from src/goto-programs/convert_nondet.h rename to src/java_bytecode/convert_java_nondet.h index 7bd3c2ce3ce..8edbcc26627 100644 --- a/src/goto-programs/convert_nondet.h +++ b/src/java_bytecode/convert_java_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 // size_t #include @@ -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 fd461467060..2be5ebd63c6 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 -#include #include #include #include @@ -54,6 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include