scripts/cpa.sh -heap 50000M -noout -disable-java-assertions -predicateAnalysis-PredAbsRefiner-ABEl -setprop cpa.predicate.handlePointerAliasing=false -64 -timelimit 900s -stats -spec test/programs/benchmarks/ldv-linux-3.4-simple/ALL.prp test/programs/benchmarks/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--algos--i2c-algo-pca.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c -------------------------------------------------------------------------------- Running CPAchecker with Java heap of size 50000M. Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO) CPAchecker 1.4-svn (OpenJDK 64-Bit Server VM 1.7.0_65) started (CPAchecker.run, INFO) line 2492: Function pointer *__cil_tmp5 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2502: Function pointer *__cil_tmp9 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2512: Function pointer *__cil_tmp13 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2820: Function pointer *__cil_tmp10 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2905: Function pointer *__cil_tmp29 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2917: Function pointer *__cil_tmp33 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5162: Function pointer *__cil_tmp127 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5172: Function pointer *__cil_tmp131 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5182: Function pointer *__cil_tmp135 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5192: Function pointer *__cil_tmp139 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5202: Function pointer *__cil_tmp143 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5212: Function pointer *__cil_tmp147 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5222: Function pointer *__cil_tmp151 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4941: Function pointer *__cil_tmp68 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4442: Function pointer *__cil_tmp9 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4452: Function pointer *__cil_tmp13 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4462: Function pointer *__cil_tmp17 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4472: Function pointer *__cil_tmp21 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4482: Function pointer *__cil_tmp25 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4492: Function pointer *__cil_tmp29 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2638: Function pointer *__cil_tmp7 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2680: Function pointer *__cil_tmp13 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3137: Function pointer *__cil_tmp8 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3160: Function pointer *__cil_tmp12 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3064: Function pointer *__cil_tmp8 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2549: Function pointer *__cil_tmp7 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2591: Function pointer *__cil_tmp13 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2722: Function pointer *__cil_tmp6 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2764: Function pointer *__cil_tmp12 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 2970: Function pointer *__cil_tmp8 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3012: Function pointer *__cil_tmp15 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3024: Function pointer *__cil_tmp20 with type void (*)(void *, int, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3398: Function pointer *__cil_tmp34 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4340: Function pointer *__cil_tmp172 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 4350: Function pointer *__cil_tmp176 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 3698: Function pointer *__cil_tmp91 with type int (*)(void *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) Handling of pointer aliasing is disabled, analysis is unsound if aliased pointers exist. (PredicateCPA:PathFormulaManagerImpl., WARNING) Using predicate analysis with SMTInterpol 2.1-174-ga199d47-comp and JFactory 1.21. (PredicateCPA:PredicateCPA., INFO) Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner., INFO) The following configuration options were specified but are not used: cpa.predicate.memoryAllocationsAlwaysSucceed cpa.predicate.maxPreFilledAllocationSize (CPAchecker.printConfigurationWarnings, WARNING) Starting analysis ... (CPAchecker.runAlgorithm, INFO) Program contains array, or pointer (multiple level of indirection), or field (enable handleFieldAccess and handleFieldAliasing) access; analysis is imprecise in case of aliasing. (PredicateCPA:CtoFormulaConverter.makeVariableUnsafe, WARNING) Assuming external function ldv_initialize to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 3398: Ignoring call via function pointer pca_xfer::__cil_tmp34 for which no suitable target was found in line: state = (*__cil_tmp34)(__cil_tmp35, 0); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3398: Ignoring function call through function pointer *__cil_tmp34: state = (*__cil_tmp34)(__cil_tmp35, 0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3698: Ignoring call via function pointer pca_xfer::__cil_tmp91 for which no suitable target was found in line: state = (*__cil_tmp91)(__cil_tmp92, 0); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3698: Ignoring function call through function pointer *__cil_tmp91: state = (*__cil_tmp91)(__cil_tmp92, 0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function dev_err to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 4282: Ignoring call via function pointer pca_xfer::__cil_tmp162 for which no suitable target was found in line: (*__cil_tmp162)(__cil_tmp163); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4282: Ignoring function call through function pointer *__cil_tmp162: (*__cil_tmp162)(__cil_tmp163); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2492: Ignoring call via function pointer pca9665_reset::__cil_tmp5 for which no suitable target was found in line: (*__cil_tmp5)(__cil_tmp6, 0, 5); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2492: Ignoring function call through function pointer *__cil_tmp5: (*__cil_tmp5)(__cil_tmp6, 0, 5); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2502: Ignoring call via function pointer pca9665_reset::__cil_tmp9 for which no suitable target was found in line: (*__cil_tmp9)(__cil_tmp10, 2, 165); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2502: Ignoring function call through function pointer *__cil_tmp9: (*__cil_tmp9)(__cil_tmp10, 2, 165); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2512: Ignoring call via function pointer pca9665_reset::__cil_tmp13 for which no suitable target was found in line: (*__cil_tmp13)(__cil_tmp14, 2, 90); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2512: Ignoring function call through function pointer *__cil_tmp13: (*__cil_tmp13)(__cil_tmp14, 2, 90); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4243: Ignoring call via function pointer pca_xfer::__cil_tmp156 for which no suitable target was found in line: (*__cil_tmp156)(__cil_tmp157); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4243: Ignoring function call through function pointer *__cil_tmp156: (*__cil_tmp156)(__cil_tmp157); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4204: Ignoring call via function pointer pca_xfer::__cil_tmp150 for which no suitable target was found in line: (*__cil_tmp150)(__cil_tmp151); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4204: Ignoring function call through function pointer *__cil_tmp150: (*__cil_tmp150)(__cil_tmp151); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2722: Ignoring call via function pointer pca_stop::__cil_tmp6 for which no suitable target was found in line: tmp___7 = (*__cil_tmp6)(__cil_tmp7, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2722: Ignoring function call through function pointer *__cil_tmp6: tmp___7 = (*__cil_tmp6)(__cil_tmp7, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2764: Ignoring call via function pointer pca_stop::__cil_tmp12 for which no suitable target was found in line: (*__cil_tmp12)(__cil_tmp13, 3, sta); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2764: Ignoring function call through function pointer *__cil_tmp12: (*__cil_tmp12)(__cil_tmp13, 3, sta); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3064: Ignoring call via function pointer pca_rx_byte::__cil_tmp8 for which no suitable target was found in line: tmp___7 = (*__cil_tmp8)(__cil_tmp9, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3064: Ignoring function call through function pointer *__cil_tmp8: tmp___7 = (*__cil_tmp8)(__cil_tmp9, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2638: Ignoring call via function pointer pca_repeated_start::__cil_tmp7 for which no suitable target was found in line: tmp___7 = (*__cil_tmp7)(__cil_tmp8, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2638: Ignoring function call through function pointer *__cil_tmp7: tmp___7 = (*__cil_tmp7)(__cil_tmp8, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2680: Ignoring call via function pointer pca_repeated_start::__cil_tmp13 for which no suitable target was found in line: (*__cil_tmp13)(__cil_tmp14, 3, sta); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2680: Ignoring function call through function pointer *__cil_tmp13: (*__cil_tmp13)(__cil_tmp14, 3, sta); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2690: Ignoring call via function pointer pca_repeated_start::__cil_tmp17 for which no suitable target was found in line: tmp___8 = (*__cil_tmp17)(__cil_tmp18); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2690: Ignoring function call through function pointer *__cil_tmp17: tmp___8 = (*__cil_tmp17)(__cil_tmp18); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4442: Ignoring call via function pointer pca_probe_chip::__cil_tmp9 for which no suitable target was found in line: (*__cil_tmp9)(__cil_tmp10, 0, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4442: Ignoring function call through function pointer *__cil_tmp9: (*__cil_tmp9)(__cil_tmp10, 0, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4452: Ignoring call via function pointer pca_probe_chip::__cil_tmp13 for which no suitable target was found in line: (*__cil_tmp13)(__cil_tmp14, 2, 170); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4452: Ignoring function call through function pointer *__cil_tmp13: (*__cil_tmp13)(__cil_tmp14, 2, 170); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4462: Ignoring call via function pointer pca_probe_chip::__cil_tmp17 for which no suitable target was found in line: (*__cil_tmp17)(__cil_tmp18, 0, 4); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4462: Ignoring function call through function pointer *__cil_tmp17: (*__cil_tmp17)(__cil_tmp18, 0, 4); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4472: Ignoring call via function pointer pca_probe_chip::__cil_tmp21 for which no suitable target was found in line: (*__cil_tmp21)(__cil_tmp22, 2, 0); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4472: Ignoring function call through function pointer *__cil_tmp21: (*__cil_tmp21)(__cil_tmp22, 2, 0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4482: Ignoring call via function pointer pca_probe_chip::__cil_tmp25 for which no suitable target was found in line: (*__cil_tmp25)(__cil_tmp26, 0, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4482: Ignoring function call through function pointer *__cil_tmp25: (*__cil_tmp25)(__cil_tmp26, 0, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4492: Ignoring call via function pointer pca_probe_chip::__cil_tmp29 for which no suitable target was found in line: tmp___7 = (*__cil_tmp29)(__cil_tmp30, 2); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4492: Ignoring function call through function pointer *__cil_tmp29: tmp___7 = (*__cil_tmp29)(__cil_tmp30, 2); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5138: Ignoring call via function pointer pca_init::__cil_tmp117 for which no suitable target was found in line: (*__cil_tmp117)(__cil_tmp118); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5138: Ignoring function call through function pointer *__cil_tmp117: (*__cil_tmp117)(__cil_tmp118); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5162: Ignoring call via function pointer pca_init::__cil_tmp127 for which no suitable target was found in line: (*__cil_tmp127)(__cil_tmp128, 0, 6); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5162: Ignoring function call through function pointer *__cil_tmp127: (*__cil_tmp127)(__cil_tmp128, 0, 6); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5172: Ignoring call via function pointer pca_init::__cil_tmp131 for which no suitable target was found in line: (*__cil_tmp131)(__cil_tmp132, 2, mode); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5172: Ignoring function call through function pointer *__cil_tmp131: (*__cil_tmp131)(__cil_tmp132, 2, mode); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5182: Ignoring call via function pointer pca_init::__cil_tmp135 for which no suitable target was found in line: (*__cil_tmp135)(__cil_tmp136, 0, 2); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5182: Ignoring function call through function pointer *__cil_tmp135: (*__cil_tmp135)(__cil_tmp136, 0, 2); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5192: Ignoring call via function pointer pca_init::__cil_tmp139 for which no suitable target was found in line: (*__cil_tmp139)(__cil_tmp140, 2, tlow); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5192: Ignoring function call through function pointer *__cil_tmp139: (*__cil_tmp139)(__cil_tmp140, 2, tlow); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5202: Ignoring call via function pointer pca_init::__cil_tmp143 for which no suitable target was found in line: (*__cil_tmp143)(__cil_tmp144, 0, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5202: Ignoring function call through function pointer *__cil_tmp143: (*__cil_tmp143)(__cil_tmp144, 0, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5212: Ignoring call via function pointer pca_init::__cil_tmp147 for which no suitable target was found in line: (*__cil_tmp147)(__cil_tmp148, 2, thi); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5212: Ignoring function call through function pointer *__cil_tmp147: (*__cil_tmp147)(__cil_tmp148, 2, thi); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5222: Ignoring call via function pointer pca_init::__cil_tmp151 for which no suitable target was found in line: (*__cil_tmp151)(__cil_tmp152, 3, 64); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5222: Ignoring function call through function pointer *__cil_tmp151: (*__cil_tmp151)(__cil_tmp152, 3, 64); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4903: Ignoring call via function pointer pca_init::__cil_tmp53 for which no suitable target was found in line: (*__cil_tmp53)(__cil_tmp54); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4903: Ignoring function call through function pointer *__cil_tmp53: (*__cil_tmp53)(__cil_tmp54); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4941: Ignoring call via function pointer pca_init::__cil_tmp68 for which no suitable target was found in line: (*__cil_tmp68)(__cil_tmp69, 3, __cil_tmp70); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4941: Ignoring function call through function pointer *__cil_tmp68: (*__cil_tmp68)(__cil_tmp69, 3, __cil_tmp70); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __const_udelay to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function i2c_add_numbered_adapter to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function i2c_add_adapter to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 2549: Ignoring call via function pointer pca_start::__cil_tmp7 for which no suitable target was found in line: tmp___7 = (*__cil_tmp7)(__cil_tmp8, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2549: Ignoring function call through function pointer *__cil_tmp7: tmp___7 = (*__cil_tmp7)(__cil_tmp8, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2591: Ignoring call via function pointer pca_start::__cil_tmp13 for which no suitable target was found in line: (*__cil_tmp13)(__cil_tmp14, 3, sta); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2591: Ignoring function call through function pointer *__cil_tmp13: (*__cil_tmp13)(__cil_tmp14, 3, sta); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2601: Ignoring call via function pointer pca_start::__cil_tmp17 for which no suitable target was found in line: tmp___8 = (*__cil_tmp17)(__cil_tmp18); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2601: Ignoring function call through function pointer *__cil_tmp17: tmp___8 = (*__cil_tmp17)(__cil_tmp18); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3137: Ignoring call via function pointer pca_rx_ack::__cil_tmp8 for which no suitable target was found in line: tmp___7 = (*__cil_tmp8)(__cil_tmp9, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3137: Ignoring function call through function pointer *__cil_tmp8: tmp___7 = (*__cil_tmp8)(__cil_tmp9, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3160: Ignoring call via function pointer pca_rx_ack::__cil_tmp12 for which no suitable target was found in line: (*__cil_tmp12)(__cil_tmp13, 3, sta); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3160: Ignoring function call through function pointer *__cil_tmp12: (*__cil_tmp12)(__cil_tmp13, 3, sta); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3170: Ignoring call via function pointer pca_rx_ack::__cil_tmp16 for which no suitable target was found in line: tmp___8 = (*__cil_tmp16)(__cil_tmp17); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3170: Ignoring function call through function pointer *__cil_tmp16: tmp___8 = (*__cil_tmp16)(__cil_tmp17); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2970: Ignoring call via function pointer pca_tx_byte::__cil_tmp8 for which no suitable target was found in line: tmp___7 = (*__cil_tmp8)(__cil_tmp9, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2970: Ignoring function call through function pointer *__cil_tmp8: tmp___7 = (*__cil_tmp8)(__cil_tmp9, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3012: Ignoring call via function pointer pca_tx_byte::__cil_tmp15 for which no suitable target was found in line: (*__cil_tmp15)(__cil_tmp16, 1, __cil_tmp17); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3012: Ignoring function call through function pointer *__cil_tmp15: (*__cil_tmp15)(__cil_tmp16, 1, __cil_tmp17); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3024: Ignoring call via function pointer pca_tx_byte::__cil_tmp20 for which no suitable target was found in line: (*__cil_tmp20)(__cil_tmp21, 3, sta); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3024: Ignoring function call through function pointer *__cil_tmp20: (*__cil_tmp20)(__cil_tmp21, 3, sta); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 3034: Ignoring call via function pointer pca_tx_byte::__cil_tmp24 for which no suitable target was found in line: tmp___8 = (*__cil_tmp24)(__cil_tmp25); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 3034: Ignoring function call through function pointer *__cil_tmp24: tmp___8 = (*__cil_tmp24)(__cil_tmp25); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2820: Ignoring call via function pointer pca_address::__cil_tmp10 for which no suitable target was found in line: tmp___7 = (*__cil_tmp10)(__cil_tmp11, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2820: Ignoring function call through function pointer *__cil_tmp10: tmp___7 = (*__cil_tmp10)(__cil_tmp11, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2905: Ignoring call via function pointer pca_address::__cil_tmp29 for which no suitable target was found in line: (*__cil_tmp29)(__cil_tmp30, 1, addr); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2905: Ignoring function call through function pointer *__cil_tmp29: (*__cil_tmp29)(__cil_tmp30, 1, addr); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2917: Ignoring call via function pointer pca_address::__cil_tmp33 for which no suitable target was found in line: (*__cil_tmp33)(__cil_tmp34, 3, sta); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2917: Ignoring function call through function pointer *__cil_tmp33: (*__cil_tmp33)(__cil_tmp34, 3, sta); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 2927: Ignoring call via function pointer pca_address::__cil_tmp37 for which no suitable target was found in line: tmp___9 = (*__cil_tmp37)(__cil_tmp38); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 2927: Ignoring function call through function pointer *__cil_tmp37: tmp___9 = (*__cil_tmp37)(__cil_tmp38); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4340: Ignoring call via function pointer pca_xfer::__cil_tmp172 for which no suitable target was found in line: tmp___10 = (*__cil_tmp172)(__cil_tmp173, 3); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4340: Ignoring function call through function pointer *__cil_tmp172: tmp___10 = (*__cil_tmp172)(__cil_tmp173, 3); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4350: Ignoring call via function pointer pca_xfer::__cil_tmp176 for which no suitable target was found in line: tmp___11 = (*__cil_tmp176)(__cil_tmp177, 0); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4350: Ignoring function call through function pointer *__cil_tmp176: tmp___11 = (*__cil_tmp176)(__cil_tmp177, 0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __dynamic_dev_dbg to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function msleep to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Stopping analysis ... (CPAchecker.runAlgorithm, INFO) PredicateCPA statistics ----------------------- Number of abstractions: 28 (0% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 28 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 14 (50%) Times precision was {false}: 0 (0%) Times result was cached: 0 (0%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 14 (50%) Times result was 'false': 0 (0%) Number of strengthen sat checks: 2 Times result was 'false': 1 (50%) Number of coverage checks: 1814 BDD entailment checks: 18 Number of SMT sat checks: 2 trivial: 0 cached: 0 Max ABE block size: 130 Number of predicates discovered: 2 Number of abstraction locations: 0 Max number of predicates per location: 0 Avg number of predicates per location: 0 Total predicates per abstraction: 28 Max number of predicates per abstraction: 2 Avg number of predicates per abstraction: 2.00 Number of irrelevant predicates: 0 (0%) Number of preds handled by boolean abs: 28 (100%) Total number of models for allsat: 14 Max number of models for allsat: 1 Avg number of models for allsat: 1.00 Number of path formula cache hits: 4343 (53%) Time for post operator: 0.678s Time for path formula creation: 0.617s Actual computation: 0.579s Time for strengthen operator: 0.044s Time for satisfiability checks: 0.021s Time for prec operator: 1.598s Time for abstraction: 1.591s (Max: 0.851s, Count: 28) Boolean abstraction: 0.568s Solving time: 0.511s (Max: 0.272s) Model enumeration time: 0.047s Time for BDD construction: 0.000s (Max: 0.000s) Time for merge operator: 0.348s Time for coverage check: 0.002s Time for BDD entailment checks: 0.001s Total time for SMT solver (w/o itp): 0.579s Number of BDD nodes: 203 Size of BDD node table: 10007 Size of BDD node cleanup queue: 20 (count: 95, min: 0, max: 20, avg: 0,21) Time for BDD node cleanup: 0.000s Time for BDD garbage collection: 0.000s (in 0 runs) PrecisionBootstrap statistics ----------------------------- Init. function predicates: 0 Init. global predicates: 0 Init. location predicates: 0 AutomatonAnalysis (SVCOMP) statistics ------------------------------------- Number of states: 1 Total time for successor computation: 0.169s Automaton transfers with branching: 0 Automaton transfer successors: 28598 (count: 28598, min: 1, max: 1, avg: 1,00) [1 x 28598] CPA algorithm statistics ------------------------ Number of iterations: 6847 Max size of waitlist: 31 Average size of waitlist: 15 Number of computed successors: 7763 Max successors for one state: 2 Number of times merged: 898 Number of times stopped: 916 Number of times breaked: 1 Total time for CPA algorithm: 3.606s (Max: 1.870s) Time for choose from waitlist: 0.034s Time for precision adjustment: 1.682s Time for transfer relation: 1.169s Time for merge operator: 0.414s Time for stop operator: 0.061s Time for adding to reached set: 0.095s Predicate-Abstraction Refiner statistics ---------------------------------------- Avg. length of target path (in blocks): 2 (count: 1, min: 2, max: 2, avg: 2,00) Time for refinement: 0.062s Counterexample analysis: 0.008s (Max: 0.008s, Calls: 1) Refinement sat check: 0.007s Interpolant computation: 0.000s Error path post-processing: 0.000s Path-formulas extraction: 0.000s Building the counterexample trace: 0.008s Extracting precise counterexample: 0.000s Predicate creation: 0.000s Precision update: 0.000s ARG update: 0.000s Length of refined path (in blocks): 0 (count: 0, min: 0, max: 0, avg: 0,00) Number of affected states: 0 (count: 0, min: 0, max: 0, avg: 0,00) Length (states) of path with itp 'true': 0 (count: 0, min: 0, max: 0, avg: 0,00) Length (states) of path with itp non-trivial itp: 0 (count: 0, min: 0, max: 0, avg: 0,00) Length (states) of path with itp 'false': 0 (count: 0, min: 0, max: 0, avg: 0,00) Different non-trivial interpolants along paths: 0 (count: 0, min: 0, max: 0, avg: 0,00) Equal non-trivial interpolants along paths: 0 (count: 0, min: 0, max: 0, avg: 0,00) Different precisions along paths: 0 (count: 0, min: 0, max: 0, avg: 0,00) Equal precisions along paths: 0 (count: 0, min: 0, max: 0, avg: 0,00) Number of refs with location-based cutoff: 0 CEGAR algorithm statistics -------------------------- Number of refinements: 1 Number of successful refinements: 1 Number of failed refinements: 0 Max. size of reached set before ref.: 3423 Max. size of reached set after ref.: 1 Avg. size of reached set before ref.: 3423.00 Avg. size of reached set after ref.: 1.00 Total time for CEGAR algorithm: 3.684s Time for refinements: 0.076s Average time for refinement: 0.076s Max time for refinement: 0.076s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 0 CPAchecker general statistics ----------------------------- Number of program locations: 704 Number of functions: 24 Number of loops: 5 Size of reached set: 3426 Number of reached locations: 643 (91%) Avg states per location: 5 Max states per location: 39 (at node N0) Number of reached functions: 18 (75%) Number of partitions: 3426 Avg size of partitions: 1 Max size of partitions: 1 Number of target states: 0 Time for analysis setup: 2.834s Time for loading CPAs: 0.956s Time for loading parser: 0.342s Time for CFA construction: 1.432s Time for parsing file(s): 0.469s Time for AST to CFA: 0.569s Time for CFA sanity check: 0.000s Time for post-processing: 0.282s Time for var class.: 0.000s Time for Analysis: 3.687s CPU time for analysis: 7.780s Total time for CPAchecker: 6.523s Total CPU time for CPAchecker: 11.520s Time for Garbage Collector: 0.031s (in 1 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 529MB ( 504 MiB) max; 246MB ( 235 MiB) avg; 570MB ( 544 MiB) peak Used non-heap memory: 23MB ( 22 MiB) max; 19MB ( 18 MiB) avg; 24MB ( 23 MiB) peak Used in PS Old Gen pool: 0MB ( 0 MiB) max; 0MB ( 0 MiB) avg; 0MB ( 0 MiB) peak Allocated heap memory: 2024MB ( 1930 MiB) max; 2024MB ( 1930 MiB) avg Allocated non-heap memory: 25MB ( 24 MiB) max; 24MB ( 23 MiB) avg Total process virtual memory: 57056MB ( 54413 MiB) max; 57054MB ( 54411 MiB) avg Verification result: TRUE. No property violation found by chosen configuration. More details about the verification run can be found in the directory "./output".