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_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.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 4493: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 4498: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 4503: Dead code detected: Goto: case_4 (CFACreationUtils.addEdgeToCFA, INFO) line 4512: Dead code detected: Goto: switch_default (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 switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_4 is not reachable. (CFAFunctionBuilder.leave, INFO) line 8372: Dead code detected: Goto: while_break (CFACreationUtils.addEdgeToCFA, INFO) line 8422: Dead code detected: Goto: while_break___0 (CFACreationUtils.addEdgeToCFA, INFO) line 8480: Dead code detected: Goto: while_break___1 (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label while_break is not reachable. (CFAFunctionBuilder.leave, INFO) line 13381: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 13386: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 13396: Dead code detected: Goto: case_8 (CFACreationUtils.addEdgeToCFA, INFO) line 13400: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) line 13454: Dead code detected: Goto: switch_break (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_8 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) 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) Assuming external function __pci_register_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dmi_check_system to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function register_reboot_notifier 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 __wake_up 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 lock_fb_info to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 19522: Ignoring call via function pointer atyfb_reboot_notify::__cil_tmp20 for which no suitable target was found in line: (*__cil_tmp20)(__cil_tmp21, __cil_tmp25); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 19522: Ignoring function call through function pointer *__cil_tmp20: (*__cil_tmp20)(__cil_tmp21, __cil_tmp25); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function cfb_copyarea to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ___udelay to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function cfb_imageblit to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function cfb_fillrect to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dev_get_drvdata to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function console_lock to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 13695: Ignoring call via function pointer aty_resume_chip::__cil_tmp22 for which no suitable target was found in line: (*__cil_tmp22)(__cil_tmp23, __cil_tmp26); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13695: Ignoring function call through function pointer *__cil_tmp22: (*__cil_tmp22)(__cil_tmp23, __cil_tmp26); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 11349: Ignoring call via function pointer atyfb_set_par::__cil_tmp28 for which no suitable target was found in line: err = (*__cil_tmp28)(__cil_tmp29, pixclock, __cil_tmp32, __cil_tmp35); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11349: Ignoring function call through function pointer *__cil_tmp28: err = (*__cil_tmp28)(__cil_tmp29, pixclock, __cil_tmp32, __cil_tmp35); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 11492: Ignoring call via function pointer atyfb_set_par::__cil_tmp74 for which no suitable target was found in line: (*__cil_tmp74)(__cil_tmp75, __cil_tmp79, __cil_tmp82, __cil_tmp85); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11492: Ignoring function call through function pointer *__cil_tmp74: (*__cil_tmp74)(__cil_tmp75, __cil_tmp79, __cil_tmp82, __cil_tmp85); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 11518: Ignoring call via function pointer atyfb_set_par::__cil_tmp92 for which no suitable target was found in line: (*__cil_tmp92)(__cil_tmp93, __cil_tmp97); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11518: Ignoring function call through function pointer *__cil_tmp92: (*__cil_tmp92)(__cil_tmp93, __cil_tmp97); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) 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)