Skip to content

Commit 311d195

Browse files
Move replace_java_nondet to java_bytecode
1 parent 70031c8 commit 311d195

File tree

5 files changed

+12
-11
lines changed

5 files changed

+12
-11
lines changed

src/goto-programs/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,6 @@ SRC = basic_blocks.cpp \
5252
remove_unused_functions.cpp \
5353
remove_vector.cpp \
5454
remove_virtual_functions.cpp \
55-
replace_java_nondet.cpp \
5655
resolve_inherited_component.cpp \
5756
safety_checker.cpp \
5857
set_properties.cpp \

src/java_bytecode/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ SRC = bytecode_info.cpp \
3030
java_types.cpp \
3131
java_utils.cpp \
3232
mz_zip_archive.cpp \
33+
replace_java_nondet.cpp \
3334
select_pointer_type.cpp \
3435
# Empty last line
3536

src/goto-programs/replace_java_nondet.cpp renamed to src/java_bytecode/replace_java_nondet.cpp

+7-6
Original file line numberDiff line numberDiff line change
@@ -9,16 +9,17 @@ Author: Reuben Thomas, [email protected]
99
/// \file
1010
/// Replace Java Nondet expressions
1111

12-
#include "goto-programs/replace_java_nondet.h"
13-
#include "goto-programs/goto_convert.h"
14-
#include "goto-programs/goto_model.h"
15-
#include "goto-programs/remove_skip.h"
16-
17-
#include "util/irep_ids.h"
12+
#include "replace_java_nondet.h"
1813

1914
#include <algorithm>
2015
#include <regex>
2116

17+
#include <goto-programs/goto_convert.h>
18+
#include <goto-programs/goto_model.h>
19+
#include <goto-programs/remove_skip.h>
20+
21+
#include <util/irep_ids.h>
22+
2223
/// Holds information about any discovered nondet methods, with extreme type-
2324
/// safety.
2425
class nondet_instruction_infot final

src/goto-programs/replace_java_nondet.h renamed to src/java_bytecode/replace_java_nondet.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ Author: Reuben Thomas, [email protected]
99
/// \file
1010
/// Replace Java Nondet expressions
1111

12-
#ifndef CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H
13-
#define CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H
12+
#ifndef CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H
13+
#define CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H
1414

1515
class goto_modelt;
1616
class goto_functionst;
@@ -28,4 +28,4 @@ void replace_java_nondet(goto_functionst &);
2828
/// \param function: The goto program to modify.
2929
void replace_java_nondet(goto_model_functiont &function);
3030

31-
#endif
31+
#endif // CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H

src/jbmc/jbmc_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ Author: Daniel Kroening, [email protected]
3838
#include <goto-programs/remove_asm.h>
3939
#include <goto-programs/remove_unused_functions.h>
4040
#include <goto-programs/remove_skip.h>
41-
#include <goto-programs/replace_java_nondet.h>
4241
#include <goto-programs/set_properties.h>
4342
#include <goto-programs/show_goto_functions.h>
4443
#include <goto-programs/show_symbol_table.h>
@@ -56,6 +55,7 @@ Author: Daniel Kroening, [email protected]
5655

5756
#include <java_bytecode/java_bytecode_language.h>
5857
#include <java_bytecode/java_enum_static_init_unwind_handler.h>
58+
#include <java_bytecode/replace_java_nondet.h>
5959

6060
#include <cbmc/version.h>
6161

0 commit comments

Comments
 (0)