Merge pull request diffblue#2199 from tautschnig/simplifier-typing

tautschnig · web-flow · commit 9191b6a2a21e · 2018-05-17T22:25:27.000+01:00
Static simplification should not alter symbol types
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
@@ -12,6 +12,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #include <util/options.h>
 
 #include <goto-programs/goto_model.h>
+#include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 #include <goto-programs/write_goto_binary.h>
@@ -169,6 +170,10 @@ bool static_simplifier(
     goto_model.goto_functions.update();
   }
 
+  // restore return types before writing the binary
+  restore_returns(goto_model);
+  goto_model.goto_functions.update();
+
   m.status() << "Writing goto binary" << messaget::eom;
   return write_goto_binary(out,
                            ns.get_symbol_table(),
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
@@ -352,38 +352,9 @@ bool remove_returnst::restore_returns(
         continue;
 
       // replace "fkt#return_value=x;" by "return x;"
-      code_returnt return_code(assign.rhs());
-
-      // the assignment might be a goto target
-      i_it->make_skip();
-      i_it++;
-
-      while(!i_it->is_goto() && !i_it->is_end_function())
-      {
-        INVARIANT(
-          i_it->is_dead(),
-          "only dead statements should appear between "
-          "a return and the next goto or function end");
-        i_it++;
-      }
-
-      if(i_it->is_goto())
-      {
-        INVARIANT(
-          i_it->get_target()->is_end_function(),
-          "GOTO following return should target end of function");
-      }
-      else
-      {
-        INVARIANT(
-          i_it->is_end_function(),
-          "control-flow after assigning return value should lead directly "
-          "to end of function");
-        i_it=goto_program.instructions.insert(i_it, *i_it);
-      }
-
+      const exprt rhs = assign.rhs();
       i_it->make_return();
-      i_it->code=return_code;
+      i_it->code = code_returnt(rhs);
     }
   }
 
