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.0/ALL.prp test/programs/benchmarks/ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i -------------------------------------------------------------------------------- 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 4065: Dead code detected: Goto: while_break (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label while_break is not reachable. (CFAFunctionBuilder.leave, INFO) line 4150: Dead code detected: Goto: while_break (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label while_break is not reachable. (CFAFunctionBuilder.leave, INFO) Inline assembler ignored, analysis is probably unsound! (CFABuilder.createCFA, 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) Assuming external function ldv_initialize to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_register_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_set_interface to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dev_warn to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, 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 __init_waitqueue_head to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_get_dev to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_get_intf to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dev_set_drvdata to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ldv_undefined_pointer to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_put_intf to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_put_dev to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function request_firmware to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dev_err to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 4759: Ignoring function call through function pointer *(i1480->read): result = (*(i1480->read))(i1480, reg, 4); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function usb_control_msg to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 4772: Ignoring function call through function pointer *(i1480->write): result = (*(i1480->write))(i1480, reg, (const void *)buffer, 4); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function dev_printk to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) lines 4664-4665: Ignoring function call through function pointer *(i1480->write): tmp___0 = (*(i1480->write))(i1480, __CPAchecker_TMP_0, __CPAchecker_TMP_1, (hdr_itr->length) * 4); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) lines 4512-4513: Ignoring function call through function pointer *(i1480->read): tmp = (*(i1480->read))(i1480, (u32 )((hdr->address) + ((unsigned long)src_itr)), chunk_size); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function memcmp to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 4813: Ignoring function call through function pointer *(i1480->read): result = (*(i1480->read))(i1480, reg, 4); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 4826: Ignoring function call through function pointer *(i1480->write): result = (*(i1480->write))(i1480, reg, (const void *)buffer, 4); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function _dev_info to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function release_firmware to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function msleep to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Warning: Analysis stopped (The CPU-time limit of 900s has elapsed.) (ShutdownNotifier.shutdownIfNecessary, WARNING) Shutdown requested (The CPU-time limit of 900s has elapsed.), waiting for termination. (ForceTerminationOnShutdown$1.shutdownRequested, WARNING)