Skip to content

Commit 2fe55a3

Browse files
committed
Fix breakage introduced during rebase
1 parent 8dd731b commit 2fe55a3

4 files changed

+5
-17
lines changed

src/java_bytecode/java_bytecode_convert_method.cpp

-4
Original file line numberDiff line numberDiff line change
@@ -483,10 +483,6 @@ void java_bytecode_convert_methodt::convert(
483483
if((!m.is_abstract) && (!m.is_native))
484484
method_symbol.value=convert_instructions(m, code_type);
485485

486-
#ifdef DEBUG
487-
std::cerr << method_symbol.value.pretty() << '\n';
488-
#endif
489-
490486
remove_assert_after_generic_nondet(method_symbol.value);
491487

492488
// Replace the existing stub symbol with the real deal:

src/java_bytecode/java_bytecode_language.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -494,7 +494,8 @@ bool java_bytecode_languaget::typecheck(
494494
disable_runtime_checks,
495495
max_user_array_length,
496496
lazy_methods,
497-
lazy_methods_mode))
497+
lazy_methods_mode,
498+
string_refinement_enabled))
498499
return true;
499500
}
500501

src/java_bytecode/java_bytecode_typecheck.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,8 @@ Author: Daniel Kroening, [email protected]
2121

2222
bool java_bytecode_typecheck(
2323
symbol_tablet &symbol_table,
24-
message_handlert &message_handler);
24+
message_handlert &message_handler,
25+
bool string_refinement_enabled);
2526

2627
bool java_bytecode_typecheck(
2728
exprt &expr,
@@ -50,6 +51,7 @@ class java_bytecode_typecheckt:public typecheckt
5051
protected:
5152
symbol_tablet &symbol_table;
5253
const namespacet ns;
54+
bool string_refinement_enabled;
5355

5456
void typecheck_type_symbol(symbolt &);
5557
void typecheck_non_type_symbol(symbolt &);

src/java_bytecode/java_bytecode_typecheck_expr.cpp

-11
Original file line numberDiff line numberDiff line change
@@ -22,17 +22,6 @@ Author: Daniel Kroening, [email protected]
2222
#include "java_pointer_casts.h"
2323
#include "java_types.h"
2424

25-
java_bytecode_typecheckt::java_bytecode_typecheckt(
26-
symbol_tablet &_symbol_table,
27-
message_handlert &_message_handler,
28-
size_t _max_nondet_array_length)
29-
: typecheckt(_message_handler),
30-
symbol_table(_symbol_table),
31-
ns(symbol_table),
32-
max_nondet_array_length(_max_nondet_array_length)
33-
{
34-
}
35-
3625
/*******************************************************************\
3726
3827
Function: java_bytecode_typecheckt::typecheck_expr

0 commit comments

Comments
 (0)