Add reference allocation code for references

romainbrenguier · romainbrenguier · commit 5e92c9bb58eb · 2019-09-20T09:24:33.000+01:00
diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -755,12 +755,7 @@ static get_or_create_reference_resultt get_or_create_reference(
       reference.array_length =
         info.allocate_objects.allocate_automatic_local_object(
           java_int_type(), "user_specified_array_length");
-      code.add(code_without_referencest{code_assignt{
-        *reference.array_length, side_effect_expr_nondett{java_int_type()}}});
-      code.add(code_without_referencest{code_assumet{binary_predicate_exprt{
-        *reference.array_length, ID_ge, from_integer(0, java_int_type())}}});
-      code.add(code_without_referencest{
-        allocate_array(reference.expr, *reference.array_length, info.loc)});
+      code.add(reference_allocationt{id, info.loc});
     }
     else
     {

Original file line number	Diff line number	Diff line change
`@@ -755,12 +755,7 @@ static get_or_create_reference_resultt get_or_create_reference(`
`755`	`755`	`reference.array_length =`
`756`	`756`	`info.allocate_objects.allocate_automatic_local_object(`
`757`	`757`	`java_int_type(), "user_specified_array_length");`
`758`		`- code.add(code_without_referencest{code_assignt{`
`759`		`- *reference.array_length, side_effect_expr_nondett{java_int_type()}}});`
`760`		`- code.add(code_without_referencest{code_assumet{binary_predicate_exprt{`
`761`		`- *reference.array_length, ID_ge, from_integer(0, java_int_type())}}});`
`762`		`- code.add(code_without_referencest{`
`763`		`- allocate_array(reference.expr, *reference.array_length, info.loc)});`
	`758`	`+ code.add(reference_allocationt{id, info.loc});`
`764`	`759`	`}`
`765`	`760`	`else`
`766`	`761`	`{`