Merge pull request #155 from peterschrammel/loop-number-update

goto_functions update must recompute loop numbers

Author: Daniel Kroening

regression/cbmc-java/iterator1/iterator1.class

@@ -0,0 +1,11 @@
+import java.util.List;
+
+public class iterator1
+{
+  public void f(List<String> list)
+  {
+    int i = 0;
+    for(String s : list)
+      i++;
+  }
+}

regression/cbmc-java/iterator1/iterator1.java

@@ -0,0 +1,8 @@
+CORE
+iterator1.class
+--cover location --unwind 3 --function iterator1.f 
+^EXIT=0$
+^SIGNAL=0$
+^.*SATISFIED$
+--
+^warning: ignoring

regression/cbmc-java/iterator1/test.desc

@@ -0,0 +1,15 @@
+import java.util.List;
+
+public class iterator2
+{
+  public void f(List<List<String>> list)
+  {
+    int i = 0, j = 0;
+    for(List<String> l : list) 
+    {
+      for(String s : l)
+        i++;
+    }
+    for(j=0;j<i;j++);
+  }
+}

regression/cbmc-java/iterator2/iterator2.class

@@ -0,0 +1,8 @@
+CORE
+iterator2.class
+--cover location --unwind 3 --function iterator2.f 
+^EXIT=0$
+^SIGNAL=0$
+^.*SATISFIED$
+--
+^warning: ignoring

regression/cbmc-java/iterator2/iterator2.java

@@ -117,6 +117,7 @@ class goto_functions_templatet
     compute_incoming_edges();
     compute_target_numbers();
     compute_location_numbers();
+    compute_loop_numbers();
   }
 
   static inline irep_idt entry_point()