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/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--dpt_i2o.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 5036: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 5041: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 5046: Dead code detected: Goto: case_4 (CFACreationUtils.addEdgeToCFA, INFO) line 5055: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_2 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_4 is not reachable. (CFAFunctionBuilder.leave, INFO) line 13522: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 13527: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 13532: Dead code detected: Goto: case_4 (CFACreationUtils.addEdgeToCFA, INFO) line 13541: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_2 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_4 is not reachable. (CFAFunctionBuilder.leave, INFO) line 16689: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 16694: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 16704: Dead code detected: Goto: case_8 (CFACreationUtils.addEdgeToCFA, INFO) line 16708: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) line 16790: Dead code detected: Goto: case_1___0 (CFACreationUtils.addEdgeToCFA, INFO) line 16795: Dead code detected: Goto: case_2___0 (CFACreationUtils.addEdgeToCFA, INFO) line 16805: Dead code detected: Goto: case_8___0 (CFACreationUtils.addEdgeToCFA, INFO) line 16809: Dead code detected: Goto: switch_default___0 (CFACreationUtils.addEdgeToCFA, INFO) line 17297: Dead code detected: Goto: case_1___1 (CFACreationUtils.addEdgeToCFA, INFO) line 17302: Dead code detected: Goto: case_2___1 (CFACreationUtils.addEdgeToCFA, INFO) line 17312: Dead code detected: Goto: case_8___1 (CFACreationUtils.addEdgeToCFA, INFO) line 17316: Dead code detected: Goto: switch_default___1 (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label case_2 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1___1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1___0 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_8___1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_8___0 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_8 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_2___1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_2___0 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) Inline assembler ignored, analysis is probably unsound! (CFABuilder.createCFA, WARNING) line 22541: Function pointer *__cil_tmp22 with type void (*)(struct scsi_cmnd *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 20834: Function pointer *__cil_tmp200 with type void (*)(struct scsi_cmnd *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 8419: Function pointer *__cil_tmp87 with type void (*)(struct scsi_cmnd *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 8223: Function pointer *__cil_tmp22 with type void (*)(struct scsi_cmnd *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 19307: Function pointer *__cil_tmp47 with type void (*)(struct scsi_cmnd *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 5932: Function pointer *__cil_tmp18 with type void * (*)(struct device *, size_t , dma_addr_t *, gfp_t , struct dma_attrs *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 6031: Function pointer *__cil_tmp29 with type void (*)(struct device *, size_t , void *, dma_addr_t , struct dma_attrs *) 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) Assuming external function ldv_initialize to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_get_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function warn_slowpath_null to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function debug_dma_free_coherent to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 6031: Ignoring call via function pointer dma_free_attrs::__cil_tmp29 for which no suitable target was found in line: (*__cil_tmp29)(dev, size, vaddr, bus, attrs); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 6031: Ignoring function call through function pointer *__cil_tmp29: (*__cil_tmp29)(dev, size, vaddr, bus, attrs); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 5932: Ignoring call via function pointer dma_alloc_attrs::__cil_tmp18 for which no suitable target was found in line: memory = (*__cil_tmp18)(dev, size, dma_handle, tmp___1, attrs); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 5932: Ignoring function call through function pointer *__cil_tmp18: memory = (*__cil_tmp18)(dev, size, dma_handle, tmp___1, attrs); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function debug_dma_alloc_coherent to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function memset 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 schedule_timeout_uninterruptible to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __class_create to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __register_chrdev to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function mutex_lock_nested to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function free_irq to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function mutex_unlock to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function iounmap to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_release_regions to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_dev_put to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function device_destroy to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __unregister_chrdev to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function class_destroy to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_host_alloc to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function device_create to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __init_waitqueue_head to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_unlock_irqrestore to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function add_wait_queue to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_unlock_irq to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function schedule_timeout to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function schedule to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_lock_irq to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function remove_wait_queue to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ioremap_nocache to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_enable_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_request_regions to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_set_master to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dma_set_mask to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dma_get_required_mask to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dma_supported to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __raw_spin_lock_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function request_threaded_irq to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_dev_get to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_add_host_with_dma to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_scan_host to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_remove_host to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_unlock to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __scsi_iterate_devices to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_lock to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_device_put to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_dma_unmap to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 20834: Ignoring call via function pointer adpt_i2o_to_scsi::__cil_tmp200 for which no suitable target was found in line: (*__cil_tmp200)(cmd); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 20834: Ignoring function call through function pointer *__cil_tmp200: (*__cil_tmp200)(cmd); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __wake_up to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function scsi_adjust_queue_depth to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function might_fault to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _copy_to_user to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __builtin_alloca to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Cannot get declaration of function __builtin_alloca, ignoring calls to it. (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __builtin_object_size to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function warn_slowpath_fmt to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _copy_from_user to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)