Chalice/tests/regressions/workitem-10147.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

class Cell {
  
  var x: int;
  
  // the declaration of a method with the same name for a parameter
  // as well as a result alone does not yet cause a problem, but ...
  method problematic_method(c: Cell) returns (c: Cell)
    requires acc(c.x);
  {
  }
  
  // ... calling it leads to various 'undeclared identifier' errors
  // in boogie. (previously. now fixed by not allowing c as both in and out parameter)
  method error()
  {
    var a: Cell := new Cell;
    var b: Cell;
    
    call b := problematic_method(a);
  }
  
}