Error in loop unwinding using iterators

[mgudemann]

With the command line cbmc --cover location --unwind 3 --function iterator1.f iterator1.class, the following program unwinds the loop indefinitely:

import java.util.List;

public class iterator1
{
  public void f(List<List<String>> list)
  {
    int i = 0;
    for(List<String> l : list)
      for(String s : l)
        i++;
  }
}

leads to

Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
...

[cristina-david]

This only seems to happen for "--cover location". Without cover or even with branch cover works ok.

[peterschrammel]

fixed by #155
The instrumentations replace the location that stores the loop number. It must be recomputed afterwards.