string keyword in C and C++ specification triggers ParseMatchError

[wandernauta]

The following input causes the C and C++ front-ends to exit with a ParseMatchError:

//@ pure string cheese() = "mozzarella";

It appears that C strings (char*) and C++ strings (std::string) are not yet supported as well as Java and PVL strings are; at least, it is not entirely clear to me how the PVL string type relates to both. Still, it would probably be nice to report this with a "not yet supported" error rather than as a crash.

The missing case seems to be specifically in the convert(implicit t: ValTypeContext) method in CToCol and CPPToCol.

Mentioning the keyword 'string' outside of a specification does not trigger the ParseMatchError.

[INFO] Done: VerCors (at 15:29:33, duration: 00:00:02)
vct.parsers.err.ParseMatchError: A MatchError occurred while parsing. This likely indicates a missing case in a parser: string (of class java.lang.String)
	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 hre.io.RWFile.read(RWFile.scala:7)
	at vct.parsers.Parser.parse(Parser.scala:34)
	at vct.parsers.parser.ColCParser.parseReader(ColCParser.scala:98)
	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:140)
	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:141)
	at vct.main.stages.Parsing.run(Parsing.scala:80)
	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: 1e37de3 (dev branch)

This issue was found by fuzzing.