File tree Expand file tree Collapse file tree 2 files changed +9
-53
lines changed
Expand file tree Collapse file tree 2 files changed +9
-53
lines changed Original file line number Diff line number Diff 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-
510474Function: 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 }
Original file line number Diff line number Diff 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-
3625exprt get_nondet_bool (const typet &);
3726
3827symbolt &new_tmp_symbol (
You can’t perform that action at this time.
0 commit comments