Merge pull request #2141 from romainbrenguier/bugfix/goto-convert-mode

Make mode an argument of goto convert methods

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