File tree 1 file changed +6
-6
lines changed 1 file changed +6
-6
lines changed Original file line number Diff line number Diff line change @@ -629,11 +629,6 @@ static bool add_nondet_string_pointer_initialization(
629
629
const source_locationt &loc,
630
630
code_blockt &code)
631
631
{
632
- if (
633
- !java_string_library_preprocesst::implements_java_char_sequence_pointer (
634
- expr.type ()))
635
- return true ;
636
-
637
632
const namespacet ns (symbol_table);
638
633
const dereference_exprt obj (expr, expr.type ().subtype ());
639
634
const struct_typet &struct_type =
@@ -786,12 +781,17 @@ void java_object_factoryt::gen_nondet_pointer_init(
786
781
code_blockt non_null_inst;
787
782
788
783
if (
784
+ java_string_library_preprocesst::implements_java_char_sequence_pointer (
785
+ expr.type ()))
786
+ {
789
787
add_nondet_string_pointer_initialization (
790
788
expr,
791
789
object_factory_parameters.max_nondet_string_length ,
792
790
symbol_table,
793
791
loc,
794
- assignments))
792
+ assignments);
793
+ }
794
+ else
795
795
{
796
796
gen_pointer_target_init (
797
797
non_null_inst,
You can’t perform that action at this time.
0 commit comments