SMG crashes because of an int in place of an address
CPAchecker with SMG analysis (scripts/cpa.sh -smg program.c
) crashes while analyzing this program:
int main() {
free(0);
return 0;
}
The cause seems to be that an integer is used where an address is expected. I think two options might be good:
- Treat such cases as an error in verified program by default, with exception for 0 as an argument of
free()
(are there other exceptions?). - Treat integers as if autoconverting to addresses took place, i.e. 0 will be treated as
Null
, and unknown integer will be treated as some new symbolic address value.
See error trace
Exception in thread "main" java.lang.AssertionError: The method evaluateAddress may not be calledwith the type signed int
at org.sosy_lab.cpachecker.cpa.smg.evaluator.SMGExpressionEvaluator.evaluateAddress(SMGExpressionEvaluator.java:498)
at org.sosy_lab.cpachecker.cpa.smg.SMGBuiltins.evaluateFree(SMGBuiltins.java:527)
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallWithoutBody(SMGTransferRelation.java:772)
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleStatementEdge(SMGTransferRelation.java:736)
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleStatementEdge(SMGTransferRelation.java:112)
at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.handleStatementEdge(ForwardingTransferRelation.java:479)
at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.getAbstractSuccessorsForEdge(ForwardingTransferRelation.java:189)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:297)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:264)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:196)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88)
at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:512)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:377)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)
Edited by Петров Олег Максимович