NullPointerException in CSystemDependenceGraphBuilder
Command line:
scripts/cpa.sh -noout -heap 2000M -predicateAnalysis-slicing -timelimit 60s -stats -spec test/config/properties/unreach-label.prp test/programs/simple/builtin_overflow_functions/builtin_overflow_side_effect_result.i
Stack trace:
Exception in thread "main" java.lang.NullPointerException
at com.google.common.base.Preconditions.checkNotNull(Preconditions.java:889)
at org.sosy_lab.cpachecker.cfa.ast.AVariableDeclaration.<init>(AVariableDeclaration.java:31)
at org.sosy_lab.cpachecker.cfa.ast.c.CVariableDeclaration.<init>(CVariableDeclaration.java:41)
at org.sosy_lab.cpachecker.cfa.ast.c.CParameterDeclaration.asVariableDeclaration(CParameterDeclaration.java:54)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$Collector.visit(EdgeDefUseData.java:503)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$Collector.visit(EdgeDefUseData.java:206)
at org.sosy_lab.cpachecker.cfa.ast.c.CParameterDeclaration.accept(CParameterDeclaration.java:84)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$Collector.visit(EdgeDefUseData.java:469)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$Collector.visit(EdgeDefUseData.java:206)
at org.sosy_lab.cpachecker.cfa.ast.c.CFunctionDeclaration.accept(CFunctionDeclaration.java:102)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$Collector.visit(EdgeDefUseData.java:558)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$Collector.visit(EdgeDefUseData.java:206)
at org.sosy_lab.cpachecker.cfa.ast.c.CFunctionCallStatement.accept(CFunctionCallStatement.java:35)
at org.sosy_lab.cpachecker.util.dependencegraph.EdgeDefUseData$1.extract(EdgeDefUseData.java:147)
at org.sosy_lab.cpachecker.util.dependencegraph.GlobalPointerState.computeAddressableVariables(GlobalPointerState.java:67)
at org.sosy_lab.cpachecker.util.dependencegraph.GlobalPointerState$FlowSensitivePointerState.create(GlobalPointerState.java:358)
at org.sosy_lab.cpachecker.util.dependencegraph.GlobalPointerState.createFlowSensitive(GlobalPointerState.java:156)
at org.sosy_lab.cpachecker.util.dependencegraph.CSystemDependenceGraphBuilder.createGlobalPointerState(CSystemDependenceGraphBuilder.java:306)
at org.sosy_lab.cpachecker.util.dependencegraph.CSystemDependenceGraphBuilder.insertFlowDependencies(CSystemDependenceGraphBuilder.java:702)
at org.sosy_lab.cpachecker.util.dependencegraph.CSystemDependenceGraphBuilder.insertDependencies(CSystemDependenceGraphBuilder.java:215)
at org.sosy_lab.cpachecker.util.dependencegraph.CSystemDependenceGraphBuilder.build(CSystemDependenceGraphBuilder.java:259)
at org.sosy_lab.cpachecker.util.slicing.SlicerFactory.createDependenceGraph(SlicerFactory.java:101)
at org.sosy_lab.cpachecker.util.slicing.SlicerFactory.create(SlicerFactory.java:137)
at org.sosy_lab.cpachecker.cpa.slicing.SlicingCPA.<init>(SlicingCPA.java:103)
at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:490)
at org.sosy_lab.cpachecker.core.defaults.AutomaticCPAFactory.createInstance(AutomaticCPAFactory.java:174)
at org.sosy_lab.cpachecker.core.CPABuilder.instantiateCPAandChildren(CPABuilder.java:362)
at org.sosy_lab.cpachecker.core.CPABuilder.createAndSetChildrenCPAs(CPABuilder.java:496)
at org.sosy_lab.cpachecker.core.CPABuilder.instantiateCPAandChildren(CPABuilder.java:357)
at org.sosy_lab.cpachecker.core.CPABuilder.createAndSetChildrenCPAs(CPABuilder.java:477)
at org.sosy_lab.cpachecker.core.CPABuilder.instantiateCPAandChildren(CPABuilder.java:357)
at org.sosy_lab.cpachecker.core.CPABuilder.buildCPAs(CPABuilder.java:198)
at org.sosy_lab.cpachecker.core.CPABuilder.buildCPAs(CPABuilder.java:100)
at org.sosy_lab.cpachecker.core.CoreComponentsFactory.createCPA(CoreComponentsFactory.java:789)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:332)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:169)
What happens is that CParameterDeclaration.asVariableDeclaration()
is called and that this fails because the parameter does not have a qualified name. This is because the function that is called is external, builtin, and undeclared (__builtin_sadd_overflow
). (source)
It is likely that the code that is visible in the stack trace never actually needs the parameters / parameter names of calls to extern functions, because this have absolutely no effect on the program semantics. So the fix is likely to ignore these.