Skip to content

Commit 9a1dae0

Browse files
author
Owen Jones
committed
Remove function that's only used once
gen_nondet_init() is only used once, and is only two lines long, so get rid of it and just put those two lines. This also avoids confusion with java_object_factory::gen_nondet_init().
1 parent 4c4ccc0 commit 9a1dae0

File tree

2 files changed

+9
-53
lines changed

2 files changed

+9
-53
lines changed

src/java_bytecode/java_object_factory.cpp

+9-42
Original file line numberDiff line numberDiff line change
@@ -471,42 +471,6 @@ void java_object_factoryt::gen_nondet_array_init(
471471

472472
/*******************************************************************\
473473
474-
Function: gen_nondet_init
475-
476-
Inputs:
477-
478-
Outputs:
479-
480-
Purpose:
481-
482-
\*******************************************************************/
483-
484-
void gen_nondet_init(
485-
const exprt &expr,
486-
code_blockt &init_code,
487-
symbol_tablet &symbol_table,
488-
const source_locationt &loc,
489-
bool create_dyn_objs,
490-
bool assume_non_null,
491-
message_handlert &message_handler,
492-
size_t max_nondet_array_length)
493-
{
494-
java_object_factoryt state(
495-
init_code,
496-
assume_non_null,
497-
max_nondet_array_length,
498-
symbol_table,
499-
message_handler);
500-
state.gen_nondet_init(
501-
expr,
502-
false,
503-
"",
504-
loc,
505-
create_dyn_objs);
506-
}
507-
508-
/*******************************************************************\
509-
510474
Function: new_tmp_symbol
511475
512476
Inputs:
@@ -582,15 +546,18 @@ exprt object_factory(
582546

583547
exprt object=aux_symbol.symbol_expr();
584548

585-
gen_nondet_init(
586-
object,
549+
java_object_factoryt state(
587550
init_code,
551+
!allow_null,
552+
max_nondet_array_length,
588553
symbol_table,
589-
loc,
554+
message_handler);
555+
state.gen_nondet_init(
556+
object,
590557
false,
591-
!allow_null,
592-
message_handler,
593-
max_nondet_array_length);
558+
"",
559+
loc,
560+
false);
594561

595562
return object;
596563
}

src/java_bytecode/java_object_factory.h

-11
Original file line numberDiff line numberDiff line change
@@ -22,17 +22,6 @@ exprt object_factory(
2222
const source_locationt &,
2323
message_handlert &message_handler);
2424

25-
void gen_nondet_init(
26-
const exprt &expr,
27-
code_blockt &init_code,
28-
symbol_tablet &symbol_table,
29-
const source_locationt &,
30-
bool create_dynamic_objects,
31-
bool assume_non_null,
32-
message_handlert &message_handler,
33-
size_t max_nondet_array_length=5);
34-
35-
3625
exprt get_nondet_bool(const typet &);
3726

3827
symbolt &new_tmp_symbol(

0 commit comments

Comments
 (0)