You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A C program with a union declaration, such as the following, causes a MatchError and thus a crash:
union onion {
float goat;
char guitar;
};
It seems C and C++ unions are unsupported in general – probably for good reason! I imagine they're difficult to prove things about. However, in C++ mode, a "syntactically valid, but not supported" message is printed, with a blame pointed right at the declaration, which is a bit nicer.
vct.parsers.err.ParseMatchError: A MatchError occurred while parsing. This likely indicates a missing case in a parser: [907 867 856 847 1636 1626 1620] (of class vct.antlr4.generated.CParser$StructOrUnionSpecifier0Context)
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:95)
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] !*!*!*!*!*!*!*!*!*!*!*!
A C program with a union declaration, such as the following, causes a
MatchError
and thus a crash:It seems C and C++ unions are unsupported in general – probably for good reason! I imagine they're difficult to prove things about. However, in C++ mode, a "syntactically valid, but not supported" message is printed, with a blame pointed right at the declaration, which is a bit nicer.
Version: 077f8b9 (dev branch).
This issue was found by fuzzing (technically).
The text was updated successfully, but these errors were encountered: