Prover types and prover functions outside PVL trigger ParseMatchError

[wandernauta]

The prover_type and prover_function spec constructs are part of the grammar for all input languages, but they are only supported for (and tested with) PVL. For other input languages, an input like this causes a MatchError, which crashes VerCors:

/*@ prover_function int one() \smtlib `1`; */

I don't know how useful it would be to have prover functions and types in non-PVL languages - it appears the need has not yet come up - but at least it may be nice to show a "syntactically valid, but not supported" message in this case.

vct.parsers.err.ParseMatchError: A MatchError occurred while parsing. This likely indicates a missing case in a parser: [3125 560 501] (of class vct.antlr4.generated.JavaParser$ValProverFunctionContext)
	at vct.parsers.AntlrParser.parseAntlrStreamOrThrow(AntlrParser.scala:155)
	at vct.parsers.AntlrParser.parseAntlrStream(AntlrParser.scala:196)
	at vct.parsers.AntlrParser.parseReader(AntlrParser.scala:205)
	at vct.parsers.Parser.$anonfun$parse$1(Parser.scala:34)
	at hre.io.Readable.read(Readable.scala:21)
	at hre.io.Readable.read$(Readable.scala:18)
	at vct.options.types.PathOrStd$Path.read(PathOrStd.scala:56)
	at vct.parsers.Parser.parse(Parser.scala:34)
	at vct.main.stages.Parsing.$anonfun$run$2(Parsing.scala:139)
	at hre.progress.Progress$.$anonfun$map$2(Progress.scala:35)
	at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166)
	at hre.progress.Progress$.$anonfun$map$1(Progress.scala:35)
	at scala.collection.Iterator$$anon$9.next(Iterator.scala:584)
	at scala.collection.immutable.List.prependedAll(List.scala:153)
	at scala.collection.immutable.List$.from(List.scala:684)
	at scala.collection.immutable.List$.from(List.scala:681)
	at scala.collection.SeqFactory$Delegate.from(Factory.scala:306)
	at scala.collection.immutable.Seq$.from(Seq.scala:42)
	at scala.collection.immutable.Seq$.from(Seq.scala:39)
	at scala.collection.IterableFactory$ToFactory.fromSpecific(Factory.scala:274)
	at scala.collection.IterableOnceOps.to(IterableOnce.scala:1310)
	at scala.collection.IterableOnceOps.to$(IterableOnce.scala:1310)
	at scala.collection.AbstractIterator.to(Iterator.scala:1300)
	at vct.main.stages.Parsing.run(Parsing.scala:140)
	at vct.main.stages.Parsing.run(Parsing.scala:79)
	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: 077f8b9 (dev branch).

This issue was found by fuzzing.