AssertionError in SliceExporter: Unable to determine main function node
Occurs for all files I tried:
$ scripts/cpa.sh -generateSlice doc/examples/example.c
...
Exception in thread "Slice-Exporter" java.lang.AssertionError: Unable to determine main function node
at org.sosy_lab.cpachecker.cfa.CCfaTransformer$CfaBuilder.determineMainFunctionEntryNode(CCfaTransformer.java:547)
at org.sosy_lab.cpachecker.cfa.CCfaTransformer$CfaBuilder.createUnconnectedFunctionCfa(CCfaTransformer.java:552)
at org.sosy_lab.cpachecker.cfa.CCfaTransformer$CfaBuilder.createCfa(CCfaTransformer.java:597)
at org.sosy_lab.cpachecker.cfa.CCfaTransformer.createCfa(CCfaTransformer.java:91)
at org.sosy_lab.cpachecker.util.slicing.SliceToCfaConversion.convert(SliceToCfaConversion.java:261)
at org.sosy_lab.cpachecker.util.slicing.SliceExporter.exportToC(SliceExporter.java:91)
at org.sosy_lab.cpachecker.util.slicing.SliceExporter.export(SliceExporter.java:140)
at org.sosy_lab.cpachecker.util.slicing.SliceExporter.lambda$0(SliceExporter.java:160)
at java.base/java.lang.Thread.run(Thread.java:829)
The AssertionError
is actually throw
n and not from an assert
statement, so cannot be disabled with -disable-java-assertions
.
Edited by Philipp Wendler