context_everywhere with type error triggers CoercingRewriter$Incoercible exception

[wandernauta]

The context_everywhere clause expects a resource (or boolean) expression. If some other type of expression is given, this triggers an 'Internal type error' exception:

context_everywhere 1;
void one() {
}

vct.col.typerules.CoercingRewriter$Incoercible: Internal type error: CoercionErrors must not bubble. Expression 1 could not be coerced to `resource``

The context clause (without _everywhere) is not affected and correctly shows a type error ("Expected the type of this expression to be resource") with a blame pointing at the issue. This is what I would expect in this case as well.

The same issue shows up with other frontends (Java, C, C++).

vct.col.typerules.CoercingRewriter$Incoercible: Internal type error: CoercionErrors must not bubble. Expression `1` could not be coerced to `resource``
	at vct.col.typerules.CoercingRewriter.coerce(CoercingRewriter.scala:391)
	at vct.col.typerules.CoercingRewriter.res(CoercingRewriter.scala:436)
	at vct.col.typerules.CoercingRewriter.coerce(CoercingRewriter.scala:2669)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:17)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:17)
	at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:51)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:22)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
	at vct.col.ast.Procedure.rewrite(Node.scala:702)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
	at vct.col.ast.Procedure.rewriteDefault(Node.scala:702)
	at vct.col.ast.Procedure.rewriteDefault(Node.scala:702)
	at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:371)
	at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:375)
	at vct.col.util.Scopes.$anonfun$dispatch$3(Scopes.scala:137)
	at vct.col.util.Scopes.$anonfun$dispatch$3$adapted(Scopes.scala:136)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.util.Scopes.$anonfun$dispatch$2(Scopes.scala:136)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.collect(Scopes.scala:92)
	at vct.col.util.Scopes.dispatch(Scopes.scala:136)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$7(ProgramRewrite.scala:13)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
	at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
	at vct.col.ast.Program.rewrite(Node.scala:111)
	at vct.col.ast.ops.rewrite.ProgramRewrite.rewriteDefault(ProgramRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ProgramRewrite.rewriteDefault$(ProgramRewrite.scala:3)
	at vct.col.ast.Program.rewriteDefault(Node.scala:111)
	at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:170)
	at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:170)
	at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:51)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:6)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:6)
	at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:51)
	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:100)
	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:100)
	at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:169)
	at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:169)
	at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:51)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:5)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:5)
	at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:51)
	at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
	at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
	at vct.col.ast.Verification.rewrite(Node.scala:94)
	at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
	at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
	at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
	at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:168)
	at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:168)
	at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:51)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:4)
	at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:4)
	at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:51)
	at vct.main.stages.Transformation.liftedTree1$1(Transformation.scala:267)
	at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:267)
	at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:259)
	at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:25)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166)
	at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:25)
	at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:24)
	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:24)
	at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:259)
	at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:32)
	at vct.main.stages.Transformation.run(Transformation.scala:253)
	at vct.main.stages.Transformation.run(Transformation.scala:226)
	at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
	at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
	at hre.stages.Stages.$anonfun$run$1(Stages.scala:101)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at hre.stages.Stages.run(Stages.scala:98)
	at hre.stages.Stages.run$(Stages.scala:95)
	at hre.stages.StagesPair.run(Stages.scala:145)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64)
	at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.util.Time$.logTime(Time.scala:23)
	at vct.main.modes.Verify$.runOptions(Verify.scala:99)
	at vct.main.Main$.runMode(Main.scala:107)
	at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.io.Watch$.booleanWithWatch(Watch.scala:58)
	at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.runOptions(Main.scala:95)
	at vct.main.Main$.main(Main.scala:50)
	at vct.main.Main.main(Main.scala)
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!
[ERROR] ! VerCors has crashed !
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!

Version: 2bd3bca (dev branch).

This issue was found by fuzzing.