VerCors does not check if assign target is an lvalue

[bobismijnnaam]

Crash Message

VerCors crashed near this position. Cause follows:
  at vct.result.VerificationError$.withContext(VerificationError.scala:66)
  at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:11)
  at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
  at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
  at vct.col.ast.VerificationContext.rewrite(Node.scala:95)
  at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
  at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
  at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:95)
  at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:4)
  at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:4)
  at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
  at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
  ...
  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=false)

Arguments

assign.pvl

File Inputs

assign.pvl

class C {}
void m() {
  C c = new C();
  new C() = c;
}

Full Log

16:04:05.230 [INFO] Starting verification at 16:04:05
16:04:07.348 [INFO] Finished verification at 16:04:07 (duration: 00:00:02)
16:04:07.350 [ERROR] VerCors crashed near this position. Cause follows:
16:04:07.350 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
16:04:07.350 [ERROR] ! VerCors has crashed !
16:04:07.350 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
16:04:07.350 [ERROR] Please report this as a bug here: