Yields on PVL class constructor crashes VerCors.

[OmerSakar]

Crash Message

The sideEffects rewrite caused the AST to no longer typecheck:
======================================
32         res1,
   33         $colon$colon(tid, n),
                          [------------
   34         $colon$colon(B_1902151851),
                           ------------]
   35         Nil$(),
   36         Nil$(),
--------------------------------------
[1/2] This usage is out of scope,
--------------------------------------
⋱
  boolean B_1902151851
⋰
--------------------------------------
[2/2] since it is declared here.
======================================

  at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:137)
  at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:122)
  at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:87)
  at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
  at hre.progress.task.AbstractTask.frame(AbstractTask.scala:152)
  at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:87)
  at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:85)
  at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
  at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
  at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
  at hre.progress.Progress$.foreach(Progress.scala:85)
  at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:122)
  ...
  at vct.main.Main$.main(Main.scala:45)
  at vct.main.Main.main(Main.scala)

Version Information

• VerCors version 9999.9.9-SNAPSHOT
• At commit 32e9dbf from branch dev (changes=true)

Arguments

/Users/omer/Documents/BenignDataRaces/is_bad/testingthetest.pvl --no-infer-heap-context-into-frame --backend-file-base /Users/omer/Documents/BenignDataRaces/is_bad/testingthetest.pvl

File Inputs

/Users/omer/Documents/BenignDataRaces/is_bad/testingthetest.pvl

class Plz {    
    context N>0;
    yields boolean bc;
    constructor(int N) {
        bc = true;
    }
}

context N >= 0;
ensures |\result| == N;
ensures (∀ int i=0..|\result|; !\result[i]);
pure seq<boolean> initSeq(int N) = N == 0 ? [t:boolean] : [false]+initSeq(N-1);

context N > 0;
void main(int N) {
    boolean b;
    Plz gs = new Plz(N) yields {b=bc};
}

Full Log

15:04:06.095 [INFO] Starting verification at 15:04:06
15:04:06.162 [WARN] Caching is enabled, but results will be discarded, since there were uncommitted changes at compilation time.
15:04:16.577 [WARN] The binder `/Users/omer/Documents/BenignDataRaces/is_bad/testingthetest.pvl:11:9-:11:44`:`(∀ int i=0..|\result|; !\result[i]) contains no triggers`
15:04:16.724 [INFO] Finished verification at 15:04:16 (duration: 00:00:10)
15:04:16.790 [ERROR] The sideEffects rewrite caused the AST to no longer typecheck:
======================================
32         res1,
   33         $colon$colon(tid, n),
                          [------------
   34         $colon$colon(B_1902151851),
                           ------------]
   35         Nil$(),
   36         Nil$(),
--------------------------------------
[1/2] This usage is out of scope,
--------------------------------------
⋱
  boolean B_1902151851
⋰
--------------------------------------
[2/2] since it is declared here.
======================================

15:04:16.790 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
15:04:16.790 [ERROR] ! VerCors has crashed !
15:04:16.790 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
15:04:16.790 [ERROR] Please report this as a bug here: