From f1a5d6a96cf4b32bdcaba8e7c6af1ed86ac3baed Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 10 May 2018 14:38:24 +0000
Subject: [PATCH 01/13] Make functions non-empty so that the test remains
 stable under skip cleanup

---
 jbmc/regression/jbmc/virtual8/A.class    | Bin 222 -> 229 bytes
 jbmc/regression/jbmc/virtual8/B.class    | Bin 207 -> 214 bytes
 jbmc/regression/jbmc/virtual8/C.class    | Bin 207 -> 214 bytes
 jbmc/regression/jbmc/virtual8/D.class    | Bin 164 -> 164 bytes
 jbmc/regression/jbmc/virtual8/E.class    | Bin 164 -> 164 bytes
 jbmc/regression/jbmc/virtual8/Test.class | Bin 354 -> 361 bytes
 jbmc/regression/jbmc/virtual8/Test.java  |   6 +++---
 7 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/jbmc/regression/jbmc/virtual8/A.class b/jbmc/regression/jbmc/virtual8/A.class
index 680ceb8db5c63d43c9afdd4e7e415ccfaa5ba982..04fabdb8b88267ab5461b717167a84ddce0ebd51 100644
GIT binary patch
delta 83
zcmcb|_>@uf)W2Q(7#J9g8Th#vm>GE38F<+l_$G?#u`p|BdQNmK)a7JgWMBiTkOI<-
aK$?kp4UlAHU<Z<HU=dy*$pw;O;06F<8VQvE

delta 77
zcmaFLc#l!^)W2Q(7#J8#82Gptm>Ia)8F<(kcqfYLP4vvyVP#-sU;|1@0x=^9Zv->g
Rfg~GPfEP$|0(ndfTmTt42=4#@

diff --git a/jbmc/regression/jbmc/virtual8/B.class b/jbmc/regression/jbmc/virtual8/B.class
index 06e08d314d81d79375fefc3dea075bf1d6ac2e3d..4b2684c3869ffbac464bbf5e60281ebaeb14d8a7 100644
GIT binary patch
delta 83
zcmX@lc#To?)W2Q(7#J9g8Th#vm>GE38F<+l_$G?#u`p|BdQNmq(&c1eWMBiTkOI<-
aK$?kp4UlAHU<Z<HU=bl8$pw;O;06Fy^a*VM

delta 77
zcmcb{c%D)8)W2Q(7#J8#82Gptm>Ia)8F<(kcqfYLP4rCAVP#-sU;|1@0x=^9Zv->g
Rfg~GPKnO^30(ndfTmTK$2*&^b

diff --git a/jbmc/regression/jbmc/virtual8/C.class b/jbmc/regression/jbmc/virtual8/C.class
index 6391b1ca05c4835b79cb53ba5edb24acb3fba99d..3eaa2ecbd0b1c370215ce91b383a0dd25b55d043 100644
GIT binary patch
delta 83
zcmX@lc#To?)W2Q(7#J9g8Th#vm>GE38F<+l_$G?#u`p|BdQNmq(&c1eWMBiTkOI<-
aK$?kp4UlAHU<Z<HU=cAO$pw;O;06FzAPI2*

delta 77
zcmcb{c%D)8)W2Q(7#J8#82Gptm>Ia)8F<(kcqfYLP4rCAVP#-sU;|1@0x=^9Zv->g
Rfg~GPKnzH70(ndfTmTLN2+IHf

diff --git a/jbmc/regression/jbmc/virtual8/D.class b/jbmc/regression/jbmc/virtual8/D.class
index 9cbaf50b562e4cb9d8a1555bf85066d127d80b30..35e2de3b907842f2fdd5c13d40c12406f1d3565a 100644
GIT binary patch
delta 16
YcmZ3&xP+18)W2Q(7#J9gCvwaI05$^!`v3p{

delta 16
YcmZ3&xP+18)W2Q(7#J8#CUVRH05%5&`~Uy|

diff --git a/jbmc/regression/jbmc/virtual8/E.class b/jbmc/regression/jbmc/virtual8/E.class
index fcc8898043c61674bcd559159dbd73c987ff5e9d..eea310c5f77c425cd23c8b941281eba1a040e5cd 100644
GIT binary patch
delta 16
YcmZ3&xP+18)W2Q(7#J9gCvwaI05$^!`v3p{

delta 16
YcmZ3&xP+18)W2Q(7#J8#CUVRH05%5&`~Uy|

diff --git a/jbmc/regression/jbmc/virtual8/Test.class b/jbmc/regression/jbmc/virtual8/Test.class
index f90d0ac64b8cfb7dde24b4a84087a8e75f353d93..257b0b6cfeccf4e68f281fda5c7e3425787e6277 100644
GIT binary patch
delta 71
zcmaFF^pc6|)W2Q(7#J9g8Kft2H8M&~?9papWMJ0N^qjceMNx@?5eOL=*tE7WFokaf
WvKSe-fg~3L6Od$PV4W<@=nepZI1OR|

delta 63
zcmaFK^oWV;)W2Q(7#J8#7^Eh0H8OHe?9raM*F`~*fe{E97+AHoF)(ceG8h@Sfg~3L
O6Od$PV41AM=neoGMGRj6

diff --git a/jbmc/regression/jbmc/virtual8/Test.java b/jbmc/regression/jbmc/virtual8/Test.java
index 7d5e5b08396..f09ff2eb1b2 100644
--- a/jbmc/regression/jbmc/virtual8/Test.java
+++ b/jbmc/regression/jbmc/virtual8/Test.java
@@ -10,16 +10,16 @@ public static void main() {
 }
 
 class A {
-  void f() { }
+  int f() { return 0; }
 }
 
 
 class B extends A {
-  void f() { }
+  int f() { return 0; }
 }
 
 class C extends A {
-  void f() { }
+  int f() { return 0; }
 }
 
 class D extends C {

From b055179d2b7d0774bb1267d7a8a70bed2b293d85 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 10 May 2018 14:12:23 +0000
Subject: [PATCH 02/13] Relax test: there need not be any code at the end of
 the block to cover

---
 jbmc/regression/jbmc/generic_class_bound1/test.desc | 1 -
 1 file changed, 1 deletion(-)

diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/jbmc/regression/jbmc/generic_class_bound1/test.desc
index 0da89d44def..92f3f36c32f 100644
--- a/jbmc/regression/jbmc/generic_class_bound1/test.desc
+++ b/jbmc/regression/jbmc/generic_class_bound1/test.desc
@@ -6,7 +6,6 @@ Gn.class
 .*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block 1: FAILED
 .*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED
 .*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED
-.*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED
 .*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
 --
 --

From 9e355e9cc869227751bc6a25df62297f71b501e6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 19 Apr 2018 10:32:35 +0100
Subject: [PATCH 03/13] Use make_skip to turn an instruction into a SKIP

---
 src/analyses/goto_check.cpp          | 8 ++++++--
 src/goto-programs/set_properties.cpp | 2 +-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index c6ecab855b7..d1aa6c5b83f 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1649,12 +1649,16 @@ void goto_checkt::goto_check(
       if((is_user_provided && !enable_assertions &&
           i.source_location.get_property_class()!="error label") ||
          (!is_user_provided && !enable_built_in_assertions))
-        i.type=SKIP;
+      {
+        i.make_skip();
+      }
     }
     else if(i.is_assume())
     {
       if(!enable_assumptions)
-        i.type=SKIP;
+      {
+        i.make_skip();
+      }
     }
     else if(i.is_dead())
     {
diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp
index 19bea8f19fa..b15a54e9935 100644
--- a/src/goto-programs/set_properties.cpp
+++ b/src/goto-programs/set_properties.cpp
@@ -32,7 +32,7 @@ void set_properties(
       property_set.find(property_id);
 
     if(c_it==property_set.end())
-      it->type=SKIP;
+      it->make_skip();
     else
       property_set.erase(c_it);
   }

From 6298c189a537d0be34c60991971bb8a5e38ce70e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 19 Apr 2018 10:33:06 +0100
Subject: [PATCH 04/13] Fix wrong function description

---
 src/goto-programs/remove_returns.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 71d2761dc5c..f4555cc339f 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -314,7 +314,7 @@ code_typet original_return_type(
   return type;
 }
 
-/// turns 'return x' into an assignment to fkt#return_value
+/// turns an assignment to fkt#return_value back into 'return x'
 bool remove_returnst::restore_returns(
   goto_functionst::function_mapt::iterator f_it)
 {

From c9ead2c01d06a504c4bbdf12742bf572c5591640 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 21 Apr 2018 11:09:06 +0100
Subject: [PATCH 05/13] Avoid redundant calls to remove_skip

---
 src/goto-diff/goto_diff_parse_options.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 73cc9655594..7c0765cbc52 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -425,13 +425,13 @@ bool goto_diff_parse_optionst::process_goto_program(
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
 
-    // remove skips such that trivial GOTOs are deleted and not considered
-    // for coverage annotation:
-    remove_skip(goto_model);
-
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
+      // remove skips such that trivial GOTOs are deleted and not considered
+      // for coverage annotation:
+      remove_skip(goto_model);
+
       if(instrument_cover_goals(options, goto_model, get_message_handler()))
         return true;
     }

From 41d38bcae6fb6c97a22a3a906f5e10b6324c853a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 21 Apr 2018 11:09:29 +0100
Subject: [PATCH 06/13] Remove unused includes of remove_skip.h

---
 src/goto-instrument/accelerate/acceleration_utils.cpp | 1 -
 src/goto-programs/goto_inline.cpp                     | 1 -
 2 files changed, 2 deletions(-)

diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index 30a01ca21e4..fde3406be70 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -21,7 +21,6 @@ Author: Matt Lewis
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/wp.h>
-#include <goto-programs/remove_skip.h>
 #include <goto-programs/goto_functions.h>
 
 #include <goto-symex/goto_symex.h>
diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp
index 62957297922..5c4b1d97850 100644
--- a/src/goto-programs/goto_inline.cpp
+++ b/src/goto-programs/goto_inline.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-#include "remove_skip.h"
 #include "goto_inline_class.h"
 
 void goto_inline(

From 91d47c253c168fb08d0fa663fc7a616b7e28b53d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 20 Apr 2018 21:07:36 +0100
Subject: [PATCH 07/13] remove_skip implementation restricted to a range of
 instructions

---
 src/goto-programs/remove_skip.cpp | 62 ++++++++++++++++++++-----------
 src/goto-programs/remove_skip.h   |  5 +++
 2 files changed, 45 insertions(+), 22 deletions(-)

diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
index a41bb59aa26..3261de08eb4 100644
--- a/src/goto-programs/remove_skip.cpp
+++ b/src/goto-programs/remove_skip.cpp
@@ -69,7 +69,14 @@ bool is_skip(const goto_programt &body, goto_programt::const_targett it)
 }
 
 /// remove unnecessary skip statements
-void remove_skip(goto_programt &goto_program)
+/// \param goto_program  goto program containing the instructions to be cleaned
+/// in the range [begin, end)
+/// \param begin  iterator pointing to first instruction to be considered
+/// \param end  iterator pointing beyond last instruction to be considered
+void remove_skip(
+  goto_programt &goto_program,
+  goto_programt::targett begin,
+  goto_programt::targett end)
 {
   // This needs to be a fixed-point, as
   // removing a skip can turn a goto into a skip.
@@ -86,9 +93,7 @@ void remove_skip(goto_programt &goto_program)
 
     // remove skip statements
 
-    for(goto_programt::instructionst::iterator
-        it=goto_program.instructions.begin();
-        it!=goto_program.instructions.end();)
+    for(goto_programt::instructionst::iterator it = begin; it != end;)
     {
       goto_programt::targett old_target=it;
 
@@ -99,7 +104,7 @@ void remove_skip(goto_programt &goto_program)
       {
         // don't remove the last skip statement,
         // it could be a target
-        if(it==--goto_program.instructions.end())
+        if(it == std::prev(end))
           break;
 
         // save labels
@@ -121,23 +126,23 @@ void remove_skip(goto_programt &goto_program)
         it++;
     }
 
-    // adjust gotos
-
-    Forall_goto_program_instructions(i_it, goto_program)
-      if(i_it->is_goto() || i_it->is_start_thread() || i_it->is_catch())
+    // adjust gotos across the full goto program body
+    for(auto &ins : goto_program.instructions)
+    {
+      if(ins.is_goto() || ins.is_start_thread() || ins.is_catch())
       {
-        for(goto_programt::instructiont::targetst::iterator
-            t_it=i_it->targets.begin();
-            t_it!=i_it->targets.end();
-            t_it++)
+        for(auto &target : ins.targets)
         {
-          new_targetst::const_iterator
-            result=new_targets.find(*t_it);
+          new_targetst::const_iterator result = new_targets.find(target);
 
           if(result!=new_targets.end())
-            *t_it=result->second;
+            target = result->second;
         }
       }
+    }
+
+    while(new_targets.find(begin) != new_targets.end())
+      ++begin;
 
     // now delete the skips -- we do so after adjusting the
     // gotos to avoid dangling targets
@@ -145,17 +150,30 @@ void remove_skip(goto_programt &goto_program)
       goto_program.instructions.erase(new_target.first);
 
     // remove the last skip statement unless it's a target
-    goto_program.compute_incoming_edges();
+    goto_program.compute_target_numbers();
+
+    if(begin != end)
+    {
+      goto_programt::targett last = std::prev(end);
+      if(begin == last)
+        ++begin;
 
-    if(
-      !goto_program.instructions.empty() &&
-      is_skip(goto_program, --goto_program.instructions.end()) &&
-      !goto_program.instructions.back().is_target())
-      goto_program.instructions.pop_back();
+      if(is_skip(goto_program, last) && !last->is_target())
+        goto_program.instructions.erase(last);
+    }
   }
   while(goto_program.instructions.size()<old_size);
 }
 
+/// remove unnecessary skip statements
+void remove_skip(goto_programt &goto_program)
+{
+  remove_skip(
+    goto_program,
+    goto_program.instructions.begin(),
+    goto_program.instructions.end());
+}
+
 /// remove unnecessary skip statements
 void remove_skip(goto_functionst &goto_functions)
 {
diff --git a/src/goto-programs/remove_skip.h b/src/goto-programs/remove_skip.h
index 6ff55bf3e03..8390ddcaa3b 100644
--- a/src/goto-programs/remove_skip.h
+++ b/src/goto-programs/remove_skip.h
@@ -22,4 +22,9 @@ void remove_skip(goto_programt &);
 void remove_skip(goto_functionst &);
 void remove_skip(goto_modelt &);
 
+void remove_skip(
+  goto_programt &goto_program,
+  goto_programt::targett begin,
+  const goto_programt::targett end);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H

From cfb733a8a2e120d91a8354287e1c687874012dab Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 21 Apr 2018 11:12:22 +0100
Subject: [PATCH 08/13] Make remove_skip call goto_program.update()

All invocations of remove_skip do this immediately after calling remove_skip,
which just complicates the protocol of using remove_skip.
---
 src/goto-programs/remove_skip.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
index 3261de08eb4..39f8b8a6beb 100644
--- a/src/goto-programs/remove_skip.cpp
+++ b/src/goto-programs/remove_skip.cpp
@@ -172,13 +172,18 @@ void remove_skip(goto_programt &goto_program)
     goto_program,
     goto_program.instructions.begin(),
     goto_program.instructions.end());
+
+  goto_program.update();
 }
 
 /// remove unnecessary skip statements
 void remove_skip(goto_functionst &goto_functions)
 {
   Forall_goto_functions(f_it, goto_functions)
-    remove_skip(f_it->second.body);
+    remove_skip(
+      f_it->second.body,
+      f_it->second.body.instructions.begin(),
+      f_it->second.body.instructions.end());
 
   // we may remove targets
   goto_functions.update();
@@ -188,4 +193,3 @@ void remove_skip(goto_modelt &goto_model)
 {
   remove_skip(goto_model.goto_functions);
 }
-

From e9cdffd4b8433633f420acfb92b5d43e846ffded Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 21 Apr 2018 11:07:46 +0100
Subject: [PATCH 09/13] remove_skip includes goto_{program,functions}.update(),
 avoid redundant calls

---
 jbmc/src/jbmc/jbmc_parse_options.cpp                  | 1 -
 src/goto-analyzer/static_simplifier.cpp               | 7 ++-----
 src/goto-diff/change_impact.cpp                       | 1 -
 src/goto-diff/goto_diff_parse_options.cpp             | 1 -
 src/goto-instrument/accelerate/scratch_program.cpp    | 1 -
 src/goto-instrument/full_slicer.cpp                   | 1 -
 src/goto-instrument/goto_instrument_parse_options.cpp | 1 -
 src/goto-instrument/model_argc_argv.cpp               | 2 --
 src/goto-instrument/reachability_slicer.cpp           | 1 -
 src/goto-programs/remove_function_pointers.cpp        | 3 ---
 src/goto-programs/slice_global_inits.cpp              | 1 -
 11 files changed, 2 insertions(+), 18 deletions(-)

diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index a498ab73879..26488b50ff5 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -983,7 +983,6 @@ bool jbmc_parse_optionst::process_goto_functions(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   catch(const char *e)
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index ebda62896dd..d83026698a4 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -158,16 +158,13 @@ bool static_simplifier(
     m.status() << "Removing unreachable instructions" << messaget::eom;
 
     // Removes goto false
-    remove_skip(goto_model.goto_functions);
-    goto_model.goto_functions.update();
+    remove_skip(goto_model);
 
     // Convert unreachable to skips
     remove_unreachable(goto_model.goto_functions);
-    goto_model.goto_functions.update();
 
     // Remove all of the new skips
-    remove_skip(goto_model.goto_functions);
-    goto_model.goto_functions.update();
+    remove_skip(goto_model);
   }
 
   // restore return types before writing the binary
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
index 32ce14e28fc..e9e00bab388 100644
--- a/src/goto-diff/change_impact.cpp
+++ b/src/goto-diff/change_impact.cpp
@@ -132,7 +132,6 @@ void full_slicert::operator()(
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 7c0765cbc52..4fae66c5650 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -445,7 +445,6 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   catch(const char *e)
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 6774f255c05..5f4ba509667 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -29,7 +29,6 @@ bool scratch_programt::check_sat(bool do_slice)
   add_instruction(END_FUNCTION);
 
   remove_skip(*this);
-  update();
 
 #ifdef DEBUG
   std::cout << "Checking following program for satness:\n";
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 43e60c030e3..ae7b8139fc8 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -364,7 +364,6 @@ void full_slicert::operator()(
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 void full_slicer(
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 013a206a00b..38191073a5d 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -707,7 +707,6 @@ int goto_instrument_parse_optionst::doit()
       accelerate_functions(
         goto_model, get_message_handler(), cmdline.isset("z3"));
       remove_skip(goto_model);
-      goto_model.goto_functions.update();
     }
 
     if(cmdline.isset("horn-encoding"))
diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp
index eab95aed6a8..2ab51aff310 100644
--- a/src/goto-instrument/model_argc_argv.cpp
+++ b/src/goto-instrument/model_argc_argv.cpp
@@ -182,8 +182,6 @@ bool model_argc_argv(
 
   // update counters etc.
   remove_skip(start);
-  start.compute_loop_numbers();
-  goto_model.goto_functions.update();
 
   return false;
 }
diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp
index 2f65d0b4893..788e1fa52d6 100644
--- a/src/goto-instrument/reachability_slicer.cpp
+++ b/src/goto-instrument/reachability_slicer.cpp
@@ -206,7 +206,6 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 /// Perform reachability slicing on goto_model, with respect to the
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index ff8f7292f17..e426a36ad59 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -451,10 +451,7 @@ bool remove_function_pointerst::remove_function_pointers(
     }
 
   if(did_something)
-  {
     remove_skip(goto_program);
-    goto_program.update();
-  }
 
   return did_something;
 }
diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp
index 87d92c33a6d..0c51b77fca8 100644
--- a/src/goto-programs/slice_global_inits.cpp
+++ b/src/goto-programs/slice_global_inits.cpp
@@ -88,5 +88,4 @@ void slice_global_inits(goto_modelt &goto_model)
   }
 
   remove_skip(goto_functions);
-  goto_functions.update();
 }

From 533775c97dc6b9bdb442edd8fd35a5b0be91496e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 19 Apr 2018 10:37:01 +0100
Subject: [PATCH 10/13] Remove redundant calls to
 compute_{location,loop}_numbers

---
 jbmc/src/java_bytecode/replace_java_nondet.cpp | 4 ----
 src/goto-programs/remove_virtual_functions.cpp | 6 +-----
 2 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
index 6d0e23210c1..01ae988493e 100644
--- a/jbmc/src/java_bytecode/replace_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -288,8 +288,6 @@ void replace_java_nondet(goto_model_functiont &function)
   goto_programt &program = function.get_goto_function().body;
   replace_java_nondet(program);
 
-  function.compute_location_numbers();
-
   remove_skip(program);
 }
 
@@ -300,8 +298,6 @@ void replace_java_nondet(goto_functionst &goto_functions)
     replace_java_nondet(goto_program.second.body);
   }
 
-  goto_functions.compute_location_numbers();
-
   remove_skip(goto_functions);
 }
 
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 8059f7cb558..59bad605eb0 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -536,11 +536,7 @@ void remove_virtual_functions(goto_model_functiont &function)
   class_hierarchyt class_hierarchy;
   class_hierarchy(function.get_symbol_table());
   remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
-  bool changed = rvf.remove_virtual_functions(
-    function.get_goto_function().body);
-  // Give fresh location numbers to `function`, in case it has grown:
-  if(changed)
-    function.compute_location_numbers();
+  rvf.remove_virtual_functions(function.get_goto_function().body);
 }
 
 void remove_virtual_function(

From 6bac80e4e22928ae9776ee85f25b0bd176c49f9d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 19 Apr 2018 10:37:44 +0100
Subject: [PATCH 11/13] Run remove_skip in passes that may introduce skips

The only passes left out are set_properties and remove_unreachable as the caller
may still find value in those instructions replaced by a skip. (This need not be
true and it may as well be safe to run remove_skip for those as well.)

Fixes: #2067
---
 jbmc/src/java_bytecode/remove_exceptions.cpp  | 32 ++++++++---
 src/analyses/goto_check.cpp                   | 10 ++++
 src/goto-instrument/cover.cpp                 |  4 +-
 .../goto_instrument_parse_options.cpp         |  7 ++-
 .../generate_function_bodies.cpp              |  4 ++
 src/goto-programs/remove_asm.cpp              |  7 +++
 src/goto-programs/remove_returns.cpp          |  8 +++
 .../remove_virtual_functions.cpp              | 55 +++++++++++++------
 src/goto-programs/remove_virtual_functions.h  |  4 +-
 src/goto-programs/string_instrumentation.cpp  |  4 +-
 10 files changed, 100 insertions(+), 35 deletions(-)

diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
index 9b6801128c2..25ee5b2985c 100644
--- a/jbmc/src/java_bytecode/remove_exceptions.cpp
+++ b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -26,6 +26,8 @@ Date:   December 2016
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include <analyses/uncaught_exceptions_analysis.h>
 
 /// Lowers high-level exception descriptions into low-level operations suitable
@@ -122,13 +124,13 @@ class remove_exceptionst
     const stack_catcht &stack_catch,
     const std::vector<exprt> &locals);
 
-  void instrument_throw(
+  bool instrument_throw(
     goto_programt &goto_program,
     const goto_programt::targett &,
     const stack_catcht &,
     const std::vector<exprt> &);
 
-  void instrument_function_call(
+  bool instrument_function_call(
     goto_programt &goto_program,
     const goto_programt::targett &,
     const stack_catcht &,
@@ -369,7 +371,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
 
 /// instruments each throw with conditional GOTOS to the corresponding
 /// exception handlers
-void remove_exceptionst::instrument_throw(
+bool remove_exceptionst::instrument_throw(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const remove_exceptionst::stack_catcht &stack_catch,
@@ -387,7 +389,7 @@ void remove_exceptionst::instrument_throw(
   // and this may reduce the instrumentation considerably if the programmer
   // used assertions)
   if(assertion_error)
-    return;
+    return false;
 
   add_exception_dispatch_sequence(
     goto_program, instr_it, stack_catch, locals);
@@ -403,11 +405,13 @@ void remove_exceptionst::instrument_throw(
   // now turn the `throw' into `assignment'
   instr_it->type=ASSIGN;
   instr_it->code=assignment;
+
+  return true;
 }
 
 /// instruments each function call that may escape exceptions with conditional
 /// GOTOS to the corresponding exception handlers
-void remove_exceptionst::instrument_function_call(
+bool remove_exceptionst::instrument_function_call(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const stack_catcht &stack_catch,
@@ -441,7 +445,11 @@ void remove_exceptionst::instrument_function_call(
     t_null->source_location=instr_it->source_location;
     t_null->function=instr_it->function;
     t_null->guard=eq_null;
+
+    return true;
   }
+
+  return false;
 }
 
 /// instruments throws, function calls that may escape exceptions and exception
@@ -460,6 +468,8 @@ void remove_exceptionst::instrument_exceptions(
   bool program_or_callees_may_throw =
     function_or_callees_may_throw(goto_program);
 
+  bool did_something = false;
+
   Forall_goto_program_instructions(instr_it, goto_program)
   {
     if(instr_it->is_decl())
@@ -537,18 +547,22 @@ void remove_exceptionst::instrument_exceptions(
           "CATCH opcode should be one of push-catch, pop-catch, landingpad");
       }
       instr_it->make_skip();
+      did_something = true;
     }
     else if(instr_it->type==THROW)
     {
-      instrument_throw(
-        goto_program, instr_it, stack_catch, locals);
+      did_something |=
+        instrument_throw(goto_program, instr_it, stack_catch, locals);
     }
     else if(instr_it->type==FUNCTION_CALL)
     {
-      instrument_function_call(
-        goto_program, instr_it, stack_catch, locals);
+      did_something |=
+        instrument_function_call(goto_program, instr_it, stack_catch, locals);
     }
   }
+
+  if(did_something)
+    remove_skip(goto_program);
 }
 
 void remove_exceptionst::operator()(goto_functionst &goto_functions)
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index d1aa6c5b83f..4b47085b745 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -31,6 +31,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include "local_bitvector_analysis.h"
 
 class goto_checkt
@@ -1501,6 +1503,8 @@ void goto_checkt::goto_check(
   assertions.clear();
   mode = _mode;
 
+  bool did_something = false;
+
   local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
   local_bitvector_analysis=&local_bitvector_analysis_obj;
 
@@ -1651,6 +1655,7 @@ void goto_checkt::goto_check(
          (!is_user_provided && !enable_built_in_assertions))
       {
         i.make_skip();
+        did_something = true;
       }
     }
     else if(i.is_assume())
@@ -1658,6 +1663,7 @@ void goto_checkt::goto_check(
       if(!enable_assumptions)
       {
         i.make_skip();
+        did_something = true;
       }
     }
     else if(i.is_dead())
@@ -1745,6 +1751,7 @@ void goto_checkt::goto_check(
     }
 
     // insert new instructions -- make sure targets are not moved
+    did_something |= !new_code.instructions.empty();
 
     while(!new_code.instructions.empty())
     {
@@ -1753,6 +1760,9 @@ void goto_checkt::goto_check(
       it++;
     }
   }
+
+  if(did_something)
+    remove_skip(goto_program);
 }
 
 void goto_check(
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index 6cebedc173d..f2694a587a5 100644
--- a/src/goto-instrument/cover.cpp
+++ b/src/goto-instrument/cover.cpp
@@ -20,6 +20,8 @@ Date: May 2016
 #include <util/options.h>
 #include <util/deprecate.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include "cover_basic_blocks.h"
 
 /// Applies instrumenters to given goto program
@@ -293,7 +295,7 @@ static void instrument_cover_goals(
   }
 
   if(changed)
-    function.body.update();
+    remove_skip(function.body);
 }
 
 /// Instruments a single goto program based on the given configuration
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 38191073a5d..38e5c8ee588 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -174,9 +174,6 @@ int goto_instrument_parse_optionst::doit()
         goto_unwindt goto_unwind;
         goto_unwind(goto_model, unwindset, unwind_strategy);
 
-        goto_model.goto_functions.update();
-        goto_model.goto_functions.compute_loop_numbers();
-
         if(cmdline.isset("log"))
         {
           std::string filename=cmdline.get_value("log");
@@ -202,6 +199,10 @@ int goto_instrument_parse_optionst::doit()
             std::cout << result << '\n';
           }
         }
+
+        // goto_unwind holds references to instructions, only do remove_skip
+        // after having generated the log above
+        remove_skip(goto_model);
       }
     }
 
diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp
index aca0ed19aba..d6cf18d5987 100644
--- a/src/goto-programs/generate_function_bodies.cpp
+++ b/src/goto-programs/generate_function_bodies.cpp
@@ -13,6 +13,8 @@ Author: Diffblue Ltd.
 #include <util/make_unique.h>
 #include <util/string_utils.h>
 
+#include "remove_skip.h"
+
 void generate_function_bodiest::generate_function_body(
   goto_functiont &function,
   symbol_tablet &symbol_table,
@@ -307,6 +309,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     }
     auto end_function_instruction = add_instruction();
     end_function_instruction->make_end_function();
+
+    remove_skip(function.body);
   }
 
 private:
diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp
index 8df9d6429e8..c863adde77f 100644
--- a/src/goto-programs/remove_asm.cpp
+++ b/src/goto-programs/remove_asm.cpp
@@ -20,6 +20,7 @@ Date:   December 2014
 #include <assembler/assembler_parser.h>
 
 #include "goto_model.h"
+#include "remove_skip.h"
 
 class remove_asmt
 {
@@ -280,6 +281,8 @@ void remove_asmt::process_instruction(
 void remove_asmt::process_function(
   goto_functionst::goto_functiont &goto_function)
 {
+  bool did_something = false;
+
   Forall_goto_program_instructions(it, goto_function.body)
   {
     if(it->is_other() && it->code.get_statement()==ID_asm)
@@ -287,6 +290,7 @@ void remove_asmt::process_function(
       goto_programt tmp_dest;
       process_instruction(*it, tmp_dest);
       it->make_skip();
+      did_something = true;
 
       goto_programt::targett next=it;
       next++;
@@ -294,6 +298,9 @@ void remove_asmt::process_function(
       goto_function.body.destructive_insert(next, tmp_dest);
     }
   }
+
+  if(did_something)
+    remove_skip(goto_function.body);
 }
 
 /// removes assembler
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index f4555cc339f..1544114d37f 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -17,6 +17,8 @@ Date:   September 2009
 
 #include "goto_model.h"
 
+#include "remove_skip.h"
+
 class remove_returnst
 {
 public:
@@ -342,6 +344,8 @@ bool remove_returnst::restore_returns(
 
   goto_programt &goto_program=f_it->second.body;
 
+  bool did_something = false;
+
   Forall_goto_program_instructions(i_it, goto_program)
   {
     if(i_it->is_assign())
@@ -355,9 +359,13 @@ bool remove_returnst::restore_returns(
       const exprt rhs = assign.rhs();
       i_it->make_return();
       i_it->code = code_returnt(rhs);
+      did_something = true;
     }
   }
 
+  if(did_something)
+    remove_skip(goto_program);
+
   return false;
 }
 
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 59bad605eb0..3ec0bc0d4f4 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "class_identifier.h"
 #include "goto_model.h"
+#include "remove_skip.h"
 #include "resolve_inherited_component.h"
 
 class remove_virtual_functionst
@@ -29,7 +30,7 @@ class remove_virtual_functionst
 
   bool remove_virtual_functions(goto_programt &goto_program);
 
-  void remove_virtual_function(
+  goto_programt::targett remove_virtual_function(
     goto_programt &goto_program,
     goto_programt::targett target,
     const dispatch_table_entriest &functions,
@@ -43,7 +44,7 @@ class remove_virtual_functionst
 
   const class_hierarchyt &class_hierarchy;
 
-  void remove_virtual_function(
+  goto_programt::targett remove_virtual_function(
     goto_programt &goto_program,
     goto_programt::targett target);
   typedef std::function<
@@ -71,7 +72,7 @@ remove_virtual_functionst::remove_virtual_functionst(
 {
 }
 
-void remove_virtual_functionst::remove_virtual_function(
+goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   goto_programt &goto_program,
   goto_programt::targett target)
 {
@@ -89,7 +90,7 @@ void remove_virtual_functionst::remove_virtual_function(
   dispatch_table_entriest functions;
   get_functions(function, functions);
 
-  remove_virtual_function(
+  return remove_virtual_function(
     goto_program,
     target,
     functions,
@@ -118,7 +119,7 @@ static void create_static_function_call(
     call.arguments()[0].make_typecast(need_type);
 }
 
-void remove_virtual_functionst::remove_virtual_function(
+goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   goto_programt &goto_program,
   goto_programt::targett target,
   const dispatch_table_entriest &functions,
@@ -130,10 +131,13 @@ void remove_virtual_functionst::remove_virtual_function(
   const code_function_callt &code=
     to_code_function_call(target->code);
 
+  goto_programt::targett next_target = std::next(target);
+
   if(functions.empty())
   {
     target->make_skip();
-    return; // give up
+    remove_skip(goto_program, target, next_target);
+    return next_target; // give up
   }
 
   // only one option?
@@ -141,13 +145,16 @@ void remove_virtual_functionst::remove_virtual_function(
      fallback_action==virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION)
   {
     if(functions.begin()->symbol_expr==symbol_exprt())
+    {
       target->make_skip();
+      remove_skip(goto_program, target, next_target);
+    }
     else
     {
       create_static_function_call(
         to_code_function_call(target->code), functions.front().symbol_expr, ns);
     }
-    return;
+    return next_target;
   }
 
   const auto &vcall_source_loc=target->source_location;
@@ -281,13 +288,15 @@ void remove_virtual_functionst::remove_virtual_function(
       it->source_location.set_comment(comment);
   }
 
-  goto_programt::targett next_target=target;
-  next_target++;
-
   goto_program.destructive_insert(next_target, new_code);
 
   // finally, kill original invocation
   target->make_skip();
+
+  // only remove skips within the virtual-function handling block
+  remove_skip(goto_program, target, next_target);
+
+  return next_target;
 }
 
 /// Used by get_functions to track the most-derived parent that provides an
@@ -475,7 +484,11 @@ bool remove_virtual_functionst::remove_virtual_functions(
 {
   bool did_something=false;
 
-  Forall_goto_program_instructions(target, goto_program)
+  for(goto_programt::instructionst::iterator
+      target = goto_program.instructions.begin();
+      target != goto_program.instructions.end();
+      ) // remove_virtual_function returns the next instruction to process
+  {
     if(target->is_function_call())
     {
       const code_function_callt &code=
@@ -483,15 +496,17 @@ bool remove_virtual_functionst::remove_virtual_functions(
 
       if(code.function().id()==ID_virtual_function)
       {
-        remove_virtual_function(goto_program, target);
+        target = remove_virtual_function(goto_program, target);
         did_something=true;
+        continue;
       }
     }
 
+    ++target;
+  }
+
   if(did_something)
-  {
     goto_program.update();
-  }
 
   return did_something;
 }
@@ -539,7 +554,7 @@ void remove_virtual_functions(goto_model_functiont &function)
   rvf.remove_virtual_functions(function.get_goto_function().body);
 }
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   symbol_tablet &symbol_table,
   goto_programt &goto_program,
   goto_programt::targett instruction,
@@ -550,18 +565,22 @@ void remove_virtual_function(
   class_hierarchy(symbol_table);
   remove_virtual_functionst rvf(symbol_table, class_hierarchy);
 
-  rvf.remove_virtual_function(
+  goto_programt::targett next = rvf.remove_virtual_function(
     goto_program, instruction, dispatch_table, fallback_action);
+
+  goto_program.update();
+
+  return next;
 }
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   goto_modelt &goto_model,
   goto_programt &goto_program,
   goto_programt::targett instruction,
   const dispatch_table_entriest &dispatch_table,
   virtual_dispatch_fallback_actiont fallback_action)
 {
-  remove_virtual_function(
+  return remove_virtual_function(
     goto_model.symbol_table,
     goto_program,
     instruction,
diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h
index ae5d257f6fd..5adc45c00bb 100644
--- a/src/goto-programs/remove_virtual_functions.h
+++ b/src/goto-programs/remove_virtual_functions.h
@@ -66,14 +66,14 @@ class dispatch_table_entryt
 typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
 typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   goto_modelt &goto_model,
   goto_programt &goto_program,
   goto_programt::targett instruction,
   const dispatch_table_entriest &dispatch_table,
   virtual_dispatch_fallback_actiont fallback_action);
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   symbol_tablet &symbol_table,
   goto_programt &goto_program,
   goto_programt::targett instruction,
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index e7ca8c3fb65..677a85f80e5 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/format_strings.h>
 #include <goto-programs/goto_model.h>
-
+#include <goto-programs/remove_skip.h>
 
 exprt is_zero_string(
   const exprt &what,
@@ -266,7 +266,7 @@ void string_instrumentationt::do_function_call(
     else if(identifier=="fscanf")
       do_fscanf(dest, target, call);
 
-    dest.update();
+    remove_skip(dest);
   }
 }
 

From 3f34c1aee4ff0569ba80d05a0f99e700bfd0ff15 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 21 Apr 2018 11:13:56 +0100
Subject: [PATCH 12/13] Explicitly invoke goto_program.update() where
 remove_skip is not used

---
 src/goto-programs/remove_unreachable.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp
index 07d71adf471..72fc4d7150c 100644
--- a/src/goto-programs/remove_unreachable.cpp
+++ b/src/goto-programs/remove_unreachable.cpp
@@ -41,13 +41,20 @@ void remove_unreachable(goto_programt &goto_program)
 
   // make all unreachable code a skip
   // unless it's an 'end_function'
+  bool did_something = false;
 
   Forall_goto_program_instructions(it, goto_program)
   {
     if(reachable.find(it)==reachable.end() &&
        !it->is_end_function())
+    {
       it->make_skip();
+      did_something = true;
+    }
   }
+
+  if(did_something)
+    goto_program.update();
 }
 
 /// Removes unreachable instructions from all functions.

From 15ce938e713cd3033be29377e2b27352104b9211 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 24 Apr 2018 10:21:34 +0000
Subject: [PATCH 13/13] Enable remove_skip to soundly remove skips with labels

Also add documentation to what is_skip actually does.
---
 src/goto-programs/remove_skip.cpp | 29 ++++++++++++++++++++++-------
 src/goto-programs/remove_skip.h   |  5 ++++-
 2 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
index 39f8b8a6beb..58a2ec3c134 100644
--- a/src/goto-programs/remove_skip.cpp
+++ b/src/goto-programs/remove_skip.cpp
@@ -12,12 +12,22 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "remove_skip.h"
 #include "goto_model.h"
 
-bool is_skip(const goto_programt &body, goto_programt::const_targett it)
+/// Determine whether the instruction is semantically equivalent to a skip
+/// (no-op).  This includes a skip, but also if(false) goto ..., goto next;
+///  next: ..., and (void)0.
+/// \param body  goto program containing the instruction
+/// \param it  instruction iterator that is tested for being a skip (or
+/// equivalent)
+/// \param ignore_labels  If the caller takes care of moving labels, then even
+/// skip statements carrying labels can be treated as skips (even though they
+/// may carry key information such as error labels).
+/// \return True, iff it is equivalent to a skip.
+bool is_skip(
+  const goto_programt &body,
+  goto_programt::const_targett it,
+  bool ignore_labels)
 {
-  // we won't remove labelled statements
-  // (think about error labels or the like)
-
-  if(!it->labels.empty())
+  if(!ignore_labels && !it->labels.empty())
     return false;
 
   if(it->is_skip())
@@ -100,12 +110,17 @@ void remove_skip(
       // for collecting labels
       std::list<irep_idt> labels;
 
-      while(is_skip(goto_program, it))
+      while(is_skip(goto_program, it, true))
       {
         // don't remove the last skip statement,
         // it could be a target
-        if(it == std::prev(end))
+        if(
+          it == std::prev(end) ||
+          (std::next(it)->is_end_function() &&
+           (!labels.empty() || !it->labels.empty())))
+        {
           break;
+        }
 
         // save labels
         labels.splice(labels.end(), it->labels);
diff --git a/src/goto-programs/remove_skip.h b/src/goto-programs/remove_skip.h
index 8390ddcaa3b..1ddc2fb357a 100644
--- a/src/goto-programs/remove_skip.h
+++ b/src/goto-programs/remove_skip.h
@@ -17,7 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com
 class goto_functionst;
 class goto_modelt;
 
-bool is_skip(const goto_programt &, goto_programt::const_targett);
+bool is_skip(
+  const goto_programt &,
+  goto_programt::const_targett,
+  bool ignore_labels = false);
 void remove_skip(goto_programt &);
 void remove_skip(goto_functionst &);
 void remove_skip(goto_modelt &);