utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
51 stars 24 forks source link

VerCors does not check if assign target is an lvalue #1199

Open bobismijnnaam opened 1 month ago

bobismijnnaam commented 1 month ago

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

Arguments

assign.pvl

File Inputs

assign.pvl ```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: ```