Support `icmp` instruction as branch condition in LLVM frontend
At the moment icmp
is only handled when it occurs inside a basic block (here), but not as branch condition as in br i1 icmp ...
.
That is why executing e.g.
scripts/cpa.sh -generateCFA -clang test/programs/benchmarks/busybox-1.22.0/basename-1.i
leads to an UnsupportedOperationException
with a stack trace like
Exception in thread "main" java.lang.UnsupportedOperationException: ICmp
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.createFromOpCode(CFABuilder.java:1053)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.getExpression(CFABuilder.java:1178)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.getBranchConditionForElse(CFABuilder.java:663)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.addJumpsBetweenBasicBlocks(CFABuilder.java:381)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.iterateOverFunctions(CFABuilder.java:268)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.visit(CFABuilder.java:179)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.build(CFABuilder.java:162)
at org.sosy_lab.cpachecker.cfa.parser.llvm.LlvmParser.buildCfa(LlvmParser.java:93)
...
Edited by Klara Cimbalnik