File tree Expand file tree Collapse file tree 3 files changed +4
-2
lines changed Expand file tree Collapse file tree 3 files changed +4
-2
lines changed Original file line number Diff line number Diff line change @@ -584,7 +584,7 @@ void goto_convertt::do_java_new(
584584 malloc_expr.copy_to_operands (object_size);
585585 // could use true and get rid of the code below
586586 malloc_expr.copy_to_operands (false_exprt ());
587- malloc_expr.type ()=pointer_typet (object_type );
587+ malloc_expr.type ()=rhs. type ( );
588588
589589 goto_programt::targett t_n=dest.add_instruction (ASSIGN);
590590 t_n->code =code_assignt (lhs, malloc_expr);
@@ -624,7 +624,7 @@ void goto_convertt::do_java_new_array(
624624 malloc_expr.copy_to_operands (object_size);
625625 // code use true and get rid of the code below
626626 malloc_expr.copy_to_operands (false_exprt ());
627- malloc_expr.type ()=pointer_typet (object_type );
627+ malloc_expr.type ()=rhs. type ( );
628628
629629 goto_programt::targett t_n=dest.add_instruction (ASSIGN);
630630 t_n->code =code_assignt (lhs, malloc_expr);
Original file line number Diff line number Diff line change @@ -14,6 +14,7 @@ Author: Thomas Kiley
1414
1515#include < list>
1616#include < set>
17+ #include < map>
1718#include < string>
1819#include < util/irep.h>
1920#include < util/type.h>
Original file line number Diff line number Diff line change 99#include " mm2cpp.h"
1010
1111#include < ostream>
12+ #include < map>
1213
1314#include < util/std_code.h>
1415
You can’t perform that action at this time.
0 commit comments