Make mode an argument of goto-convert functions

Fixes: #2138
This passes the mode as an argument of these functions instead of trying
to deduce it from the expression.
This avoids creating symbols with empty mode which can lead to problems
in later stages of the analysis.

Author: romainbrenguier

src/goto-instrument/model_argc_argv.cpp

@@ -143,7 +143,8 @@ bool model_argc_argv(
     to_code(value),
     goto_model.symbol_table,
     init_instructions,
-    message_handler);
+    message_handler,
+    main_symbol.mode);
 
   Forall_goto_program_instructions(it, init_instructions)
   {

src/goto-programs/builtin_functions.cpp

@@ -438,7 +438,7 @@ void goto_convertt::do_cpp_new(
       count.make_typecast(object_size.type());
 
     // might have side-effect
-    clean_expr(count, dest);
+    clean_expr(count, dest, ID_cpp);
   }
 
   exprt tmp_symbol_expr;
@@ -473,7 +473,7 @@ void goto_convertt::do_cpp_new(
     new_call.lhs()=tmp_symbol_expr;
     new_call.add_source_location()=rhs.source_location();
 
-    convert(new_call, dest);
+    convert(new_call, dest, ID_cpp);
   }
   else if(rhs.operands().size()==1)
   {
@@ -509,7 +509,7 @@ void goto_convertt::do_cpp_new(
       if(new_call.arguments()[i].type()!=code_type.parameters()[i].type())
         new_call.arguments()[i].make_typecast(code_type.parameters()[i].type());
 
-    convert(new_call, dest);
+    convert(new_call, dest, ID_cpp);
   }
   else
   {
@@ -551,7 +551,7 @@ void goto_convertt::cpp_new_initializer(
       const dereference_exprt deref_lhs(lhs, rhs.type().subtype());
 
       replace_new_object(deref_lhs, initializer);
-      convert(to_code(initializer), dest);
+      convert(to_code(initializer), dest, ID_cpp);
     }
     else
       UNREACHABLE;

src/goto-programs/convert_nondet.cpp

@@ -35,7 +35,8 @@ static goto_programt::targett insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode)
 {
   // Return if the instruction isn't an assignment
   const auto next_instr=std::next(target);
@@ -96,7 +97,8 @@ static goto_programt::targett insert_nondet_init_code(
 
   // Convert this code into goto instructions
   goto_programt new_instructions;
-  goto_convert(init_code, symbol_table, new_instructions, message_handler);
+  goto_convert(
+    init_code, symbol_table, new_instructions, message_handler, mode);
 
   // Insert the new instructions into the instruction list
   goto_program.destructive_insert(next_instr, new_instructions);
@@ -116,33 +118,37 @@ void convert_nondet(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode)
 {
   for(auto instruction_iterator=goto_program.instructions.begin(),
         end=goto_program.instructions.end();
       instruction_iterator!=end;)
   {
-    instruction_iterator=insert_nondet_init_code(
+    instruction_iterator = insert_nondet_init_code(
       goto_program,
       instruction_iterator,
       symbol_table,
       message_handler,
-      object_factory_parameters);
+      object_factory_parameters,
+      mode);
   }
 }
 
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode)
 {
   object_factory_parameterst parameters = object_factory_parameters;
   parameters.function_id = function.get_function_id();
   convert_nondet(
     function.get_goto_function().body,
     function.get_symbol_table(),
     message_handler,
-    parameters);
+    parameters,
+    mode);
 
   function.compute_location_numbers();
 }
@@ -167,7 +173,8 @@ void convert_nondet(
         f_it.second.body,
         symbol_table,
         message_handler,
-        object_factory_parameters);
+        object_factory_parameters,
+        symbol.mode);
     }
   }
 

src/goto-programs/convert_nondet.h

@@ -13,6 +13,7 @@ Author: Reuben Thomas, [email protected]
 #define CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H
 
 #include <cstddef> // size_t
+#include <util/irep.h>
 
 class goto_functionst;
 class symbol_table_baset;
@@ -48,6 +49,7 @@ void convert_nondet(
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters);
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode);
 
 #endif