Set mode in goto_convert auxiliary symbols

Author: peterschrammel

src/goto-programs/builtin_functions.cpp

@@ -468,8 +468,8 @@ void goto_convertt::do_cpp_new(
     assert(code_type.parameters().size()==1 ||
            code_type.parameters().size()==2);
 
-    const symbolt &tmp_symbol=
-      new_tmp_symbol(return_type, "new", dest, rhs.source_location());
+    const symbolt &tmp_symbol =
+      new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
 
     tmp_symbol_expr=tmp_symbol.symbol_expr();
 
@@ -499,8 +499,8 @@ void goto_convertt::do_cpp_new(
     assert(code_type.parameters().size()==2 ||
            code_type.parameters().size()==3);
 
-    const symbolt &tmp_symbol=
-      new_tmp_symbol(return_type, "new", dest, rhs.source_location());
+    const symbolt &tmp_symbol =
+      new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
 
     tmp_symbol_expr=tmp_symbol.symbol_expr();
 
@@ -663,13 +663,10 @@ void goto_convertt::do_java_new_array(
   // Must directly assign the new array to a temporary
   // because goto-symex will notice `x=side_effect_exprt` but not
   // `x=typecast_exprt(side_effect_exprt(...))`
-  symbol_exprt new_array_data_symbol=
+  symbol_exprt new_array_data_symbol =
     new_tmp_symbol(
-      data_java_new_expr.type(),
-      "new_array_data",
-      dest,
-      location)
-    .symbol_expr();
+      data_java_new_expr.type(), "new_array_data", dest, location, ID_java)
+      .symbol_expr();
   goto_programt::targett t_p2=dest.add_instruction(ASSIGN);
   t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr);
   t_p2->source_location=location;
@@ -707,8 +704,9 @@ void goto_convertt::do_java_new_array(
 
     goto_programt tmp;
 
-    symbol_exprt tmp_i=
-      new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
+    symbol_exprt tmp_i =
+      new_tmp_symbol(length.type(), "index", tmp, location, ID_java)
+        .symbol_expr();
 
     code_fort for_loop;
 
@@ -730,8 +728,9 @@ void goto_convertt::do_java_new_array(
       plus_exprt(data, tmp_i), data.type().subtype());
 
     code_blockt for_body;
-    symbol_exprt init_sym=
-      new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr();
+    symbol_exprt init_sym =
+      new_tmp_symbol(sub_type, "subarray_init", tmp, location, ID_java)
+        .symbol_expr();
 
     code_assignt init_subarray(init_sym, sub_java_new);
     code_assignt assign_subarray(

src/goto-programs/goto_clean_expr.cpp

@@ -237,8 +237,8 @@ void goto_convertt::clean_expr(
 
     if(result_is_used)
     {
-      symbolt &new_symbol=
-        new_tmp_symbol(expr.type(), "if_expr", dest, source_location);
+      symbolt &new_symbol = new_tmp_symbol(
+        expr.type(), "if_expr", dest, source_location, expr.get(ID_mode));
 
       code_assignt assignment_true;
       assignment_true.lhs()=new_symbol.symbol_expr();

src/goto-programs/goto_convert.cpp

@@ -2055,16 +2055,16 @@ symbolt &goto_convertt::new_tmp_symbol(
   const typet &type,
   const std::string &suffix,
   goto_programt &dest,
-  const source_locationt &source_location)
+  const source_locationt &source_location,
+  const irep_idt &mode)
 {
-  symbolt &new_symbol=
-    get_fresh_aux_symbol(
-      type,
-      tmp_symbol_prefix,
-      "tmp_"+suffix,
-      source_location,
-      irep_idt(),
-      symbol_table);
+  symbolt &new_symbol = get_fresh_aux_symbol(
+    type,
+    tmp_symbol_prefix,
+    "tmp_" + suffix,
+    source_location,
+    mode,
+    symbol_table);
 
   code_declt decl;
   decl.symbol()=new_symbol.symbol_expr();
@@ -2081,8 +2081,8 @@ void goto_convertt::make_temp_symbol(
 {
   const source_locationt source_location=expr.find_source_location();
 
-  symbolt &new_symbol=
-    new_tmp_symbol(expr.type(), suffix, dest, source_location);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(), suffix, dest, source_location, expr.get(ID_mode));
 
   code_assignt assignment;
   assignment.lhs()=new_symbol.symbol_expr();

src/goto-programs/goto_convert_class.h

@@ -59,7 +59,8 @@ class goto_convertt:public messaget
     const typet &type,
     const std::string &suffix,
     goto_programt &dest,
-    const source_locationt &);
+    const source_locationt &,
+    const irep_idt &mode);
 
   symbol_exprt make_compound_literal(
     const exprt &expr,

src/goto-programs/goto_convert_side_effect.cpp

@@ -522,10 +522,8 @@ void goto_convertt::remove_temporary_object(
     throw 0;
   }
 
-  symbolt &new_symbol=
-    new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location());
-
-  new_symbol.mode=expr.get(ID_mode);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(), "obj", dest, expr.find_source_location(), expr.get(ID_mode));
 
   if(expr.operands().size()==1)
   {
@@ -599,8 +597,12 @@ void goto_convertt::remove_statement_expression(
 
   source_locationt source_location=last.find_source_location();
 
-  symbolt &new_symbol=
-    new_tmp_symbol(expr.type(), "statement_expression", dest, source_location);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(),
+    "statement_expression",
+    dest,
+    source_location,
+    expr.get(ID_mode));
 
   symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
   tmp_symbol_expr.add_source_location()=source_location;