Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

C union declarations are not yet supported, trigger ParseMatchError #1291

Open
wandernauta opened this issue Dec 4, 2024 · 0 comments
Open
Labels
A-Bug F-C Frontend: C Fuzzing Found by fuzzing

Comments

@wandernauta
Copy link
Contributor

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] !*!*!*!*!*!*!*!*!*!*!*!

Version: 077f8b9 (dev branch).

This issue was found by fuzzing (technically).

@superaxander superaxander added A-Bug F-C Frontend: C Fuzzing Found by fuzzing labels Dec 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-Bug F-C Frontend: C Fuzzing Found by fuzzing
Projects
None yet
Development

No branches or pull requests

2 participants