WitnessExporter does not support backward analysis
Update on 2023-05-28
-
On 869262e8, ARGs generated from a backward analysis can be dumped correctly (file output/ARG.dot
) -
A remaining issue still needs investigation: for some programs, opening the HTML report leads to a Javascript error, cf. this comment
Original issue description
WitnessExporter
does not support backward analysis such as -predicateAnalysisBackward
and throws RuntimeException
while exporting ARGs.
An example command to trigger the exception:
./scripts/cpa.sh -spec sv-comp-reachability -predicateAnalysisBackward test/programs/benchmarks/loop-invariants/even.c
This command terminates with the following error:
Exception in thread "main" java.lang.RuntimeException: Could not determine file name based on abstract state!
at org.sosy_lab.cpachecker.cpa.arg.witnessexport.WitnessExporter.getInitialFileName(WitnessExporter.java:215)
at org.sosy_lab.cpachecker.cpa.arg.witnessexport.WitnessExporter.generateProofWitness(WitnessExporter.java:176)
at org.sosy_lab.cpachecker.cpa.arg.ARGStatistics.exportARG0(ARGStatistics.java:387)
at org.sosy_lab.cpachecker.cpa.arg.ARGStatistics.exportARG(ARGStatistics.java:370)
at org.sosy_lab.cpachecker.cpa.arg.ARGStatistics.writeOutputFiles(ARGStatistics.java:312)
at org.sosy_lab.cpachecker.util.statistics.StatisticsUtils.writeOutputFiles(StatisticsUtils.java:104)
at org.sosy_lab.cpachecker.core.MainCPAStatistics.writeOutputFiles(MainCPAStatistics.java:409)
at org.sosy_lab.cpachecker.core.CPAcheckerResult.writeOutputFiles(CPAcheckerResult.java:120)
at org.sosy_lab.cpachecker.cmdline.CPAMain.printResultAndStatistics(CPAMain.java:756)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:185)
One example piece of code that does not support backward analysis is here.
If an ARG is constructed backward, the exporter should use CFAUtils.enteringEdges()
instead.
Edited by Nian-Ze Lee