scripts/cpa.sh -heap 3000M -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--media--video--cx231xx--cx231xx-dvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c -------------------------------------------------------------------------------- Running CPAchecker with Java heap of size 3000M. 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 13428: Function pointer *__a___9 with type struct dvb_frontend * (*)(const struct mb86a20s_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13561: Function pointer *__a___10 with type struct dvb_frontend * (*)(struct dvb_frontend *, u8 , struct i2c_adapter *, struct tda18271_config *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13189: Function pointer *__a___7 with type struct dvb_frontend * (*)(const struct lgdt3305_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13322: Function pointer *__a___8 with type struct dvb_frontend * (*)(struct dvb_frontend *, u8 , struct i2c_adapter *, struct tda18271_config *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12940: Function pointer *__a___5 with type struct dvb_frontend * (*)(const struct s5h1411_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13073: Function pointer *__a___6 with type struct dvb_frontend * (*)(struct dvb_frontend *, u8 , struct i2c_adapter *, struct tda18271_config *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12715: Function pointer *__a___3 with type struct dvb_frontend * (*)(const struct s5h1432_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12848: Function pointer *__a___4 with type struct dvb_frontend * (*)(struct dvb_frontend *, u8 , struct i2c_adapter *, struct tda18271_config *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12490: Function pointer *__a___1 with type struct dvb_frontend * (*)(const struct s5h1411_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12623: Function pointer *__a___2 with type struct dvb_frontend * (*)(struct dvb_frontend *, struct i2c_adapter *, const struct xc5000_config *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12264: Function pointer *__a with type struct dvb_frontend * (*)(const struct s5h1432_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12397: Function pointer *__a___0 with type struct dvb_frontend * (*)(struct dvb_frontend *, struct i2c_adapter *, const struct xc5000_config *) 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) Assuming external function cx231xx_register_extension to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_net_release to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 11576: Ignoring call via function pointer unregister_dvb::__cil_tmp9 for which no suitable target was found in line: (*__cil_tmp9)(__cil_tmp12, __cil_tmp15); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11576: Ignoring function call through function pointer *__cil_tmp9: (*__cil_tmp9)(__cil_tmp12, __cil_tmp15); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function dvb_dmx_swfilter to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 11600: Ignoring call via function pointer unregister_dvb::__cil_tmp20 for which no suitable target was found in line: (*__cil_tmp20)(__cil_tmp23, __cil_tmp26); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11600: Ignoring function call through function pointer *__cil_tmp20: (*__cil_tmp20)(__cil_tmp23, __cil_tmp26); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function dvb_dmxdev_release to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_dmx_release to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_unregister_frontend to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_frontend_detach to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_unregister_adapter to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function cx231xx_set_mode to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function cx231xx_demod_reset to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __symbol_get to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __request_module to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 13428: Ignoring call via function pointer dvb_init::__a___9 for which no suitable target was found in line: tmp___64 = (*__a___9)(&pv_mb86a20s_config, __cil_tmp374); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13428: Ignoring function call through function pointer *__a___9: tmp___64 = (*__a___9)(&pv_mb86a20s_config, __cil_tmp374); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __symbol_put to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 13561: Ignoring call via function pointer dvb_init::__a___10 for which no suitable target was found in line: tmp___69 = (*__a___10)(__cil_tmp395, __cil_tmp396, __cil_tmp406, &pv_tda18271_config); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13561: Ignoring function call through function pointer *__a___10: tmp___69 = (*__a___10)(__cil_tmp395, __cil_tmp396, __cil_tmp406, &pv_tda18271_config); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13189: Ignoring call via function pointer dvb_init::__a___7 for which no suitable target was found in line: tmp___53 = (*__a___7)(__cil_tmp308, __cil_tmp318); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13189: Ignoring function call through function pointer *__a___7: tmp___53 = (*__a___7)(__cil_tmp308, __cil_tmp318); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13322: Ignoring call via function pointer dvb_init::__a___8 for which no suitable target was found in line: tmp___58 = (*__a___8)(__cil_tmp339, __cil_tmp340, __cil_tmp350, &hcw_tda18271_config); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13322: Ignoring function call through function pointer *__a___8: tmp___58 = (*__a___8)(__cil_tmp339, __cil_tmp340, __cil_tmp350, &hcw_tda18271_config); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12940: Ignoring call via function pointer dvb_init::__a___5 for which no suitable target was found in line: tmp___42 = (*__a___5)(__cil_tmp251, __cil_tmp261); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12940: Ignoring function call through function pointer *__a___5: tmp___42 = (*__a___5)(__cil_tmp251, __cil_tmp261); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13073: Ignoring call via function pointer dvb_init::__a___6 for which no suitable target was found in line: tmp___47 = (*__a___6)(__cil_tmp282, __cil_tmp283, __cil_tmp293, &cnxt_rde253s_tunerconfig); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13073: Ignoring function call through function pointer *__a___6: tmp___47 = (*__a___6)(__cil_tmp282, __cil_tmp283, __cil_tmp293, &cnxt_rde253s_tunerconfig); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12715: Ignoring call via function pointer dvb_init::__a___3 for which no suitable target was found in line: tmp___32 = (*__a___3)(__cil_tmp204, __cil_tmp214); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12715: Ignoring function call through function pointer *__a___3: tmp___32 = (*__a___3)(__cil_tmp204, __cil_tmp214); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12848: Ignoring call via function pointer dvb_init::__a___4 for which no suitable target was found in line: tmp___37 = (*__a___4)(__cil_tmp235, __cil_tmp236, __cil_tmp246, &cnxt_rde253s_tunerconfig); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12848: Ignoring function call through function pointer *__a___4: tmp___37 = (*__a___4)(__cil_tmp235, __cil_tmp236, __cil_tmp246, &cnxt_rde253s_tunerconfig); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12490: Ignoring call via function pointer dvb_init::__a___1 for which no suitable target was found in line: tmp___22 = (*__a___1)(__cil_tmp157, __cil_tmp167); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12490: Ignoring function call through function pointer *__a___1: tmp___22 = (*__a___1)(__cil_tmp157, __cil_tmp167); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12623: Ignoring call via function pointer dvb_init::__a___2 for which no suitable target was found in line: tmp___27 = (*__a___2)(__cil_tmp188, __cil_tmp198, __cil_tmp199); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12623: Ignoring function call through function pointer *__a___2: tmp___27 = (*__a___2)(__cil_tmp188, __cil_tmp198, __cil_tmp199); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12264: Ignoring call via function pointer dvb_init::__a for which no suitable target was found in line: tmp___12 = (*__a)(__cil_tmp110, __cil_tmp120); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12264: Ignoring function call through function pointer *__a: tmp___12 = (*__a)(__cil_tmp110, __cil_tmp120); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12397: Ignoring call via function pointer dvb_init::__a___0 for which no suitable target was found in line: tmp___17 = (*__a___0)(__cil_tmp141, __cil_tmp151, __cil_tmp152); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12397: Ignoring function call through function pointer *__a___0: tmp___17 = (*__a___0)(__cil_tmp141, __cil_tmp151, __cil_tmp152); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __mutex_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_register_adapter to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_register_frontend to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_dmx_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dvb_dmxdev_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 11250: Ignoring call via function pointer register_dvb::__cil_tmp96 for which no suitable target was found in line: result = (*__cil_tmp96)(__cil_tmp99, __cil_tmp102); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11250: Ignoring function call through function pointer *__cil_tmp96: result = (*__cil_tmp96)(__cil_tmp99, __cil_tmp102); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 11306: Ignoring call via function pointer register_dvb::__cil_tmp115 for which no suitable target was found in line: result = (*__cil_tmp115)(__cil_tmp118, __cil_tmp121); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11306: Ignoring function call through function pointer *__cil_tmp115: result = (*__cil_tmp115)(__cil_tmp118, __cil_tmp121); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 11354: Ignoring call via function pointer register_dvb::__cil_tmp131 for which no suitable target was found in line: result = (*__cil_tmp131)(__cil_tmp134, __cil_tmp137); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11354: Ignoring function call through function pointer *__cil_tmp131: result = (*__cil_tmp131)(__cil_tmp134, __cil_tmp137); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function dvb_net_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 11426: Ignoring call via function pointer register_dvb::__cil_tmp156 for which no suitable target was found in line: (*__cil_tmp156)(__cil_tmp159, __cil_tmp162); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11426: Ignoring function call through function pointer *__cil_tmp156: (*__cil_tmp156)(__cil_tmp159, __cil_tmp162); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 11453: Ignoring call via function pointer register_dvb::__cil_tmp167 for which no suitable target was found in line: (*__cil_tmp167)(__cil_tmp170, __cil_tmp173); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 11453: Ignoring function call through function pointer *__cil_tmp167: (*__cil_tmp167)(__cil_tmp170, __cil_tmp173); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function cx231xx_unregister_extension to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Stopping analysis ... (CPAchecker.runAlgorithm, INFO) PredicateCPA statistics ----------------------- Number of abstractions: 83 (1% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 83 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 7 (8%) Times precision was {false}: 0 (0%) Times result was cached: 15 (18%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 61 (73%) Times result was 'false': 8 (10%) Number of strengthen sat checks: 24 Times result was 'false': 23 (96%) Number of coverage checks: 2950 BDD entailment checks: 48 Number of SMT sat checks: 24 trivial: 0 cached: 6 Max ABE block size: 258 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: 122 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: 122 (100%) Total number of models for allsat: 55 Max number of models for allsat: 1 Avg number of models for allsat: 0.90 Number of path formula cache hits: 1071 (11%) Time for post operator: 1.766s Time for path formula creation: 1.602s Actual computation: 1.551s Time for strengthen operator: 0.252s Time for satisfiability checks: 0.181s Time for prec operator: 7.857s Time for abstraction: 7.853s (Max: 1.184s, Count: 83) Boolean abstraction: 4.838s Solving time: 4.187s (Max: 0.708s) Model enumeration time: 0.582s Time for BDD construction: 0.030s (Max: 0.016s) Time for merge operator: 1.200s Time for coverage check: 0.013s Time for BDD entailment checks: 0.000s Total time for SMT solver (w/o itp): 4.950s Number of BDD nodes: 204 Size of BDD node table: 10007 Size of BDD node cleanup queue: 70 (count: 309, min: 0, max: 25, avg: 0,23) 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.146s Automaton transfers with branching: 0 Automaton transfer successors: 26263 (count: 26263, min: 1, max: 1, avg: 1,00) [1 x 26263] CPA algorithm statistics ------------------------ Number of iterations: 8239 Max size of waitlist: 82 Average size of waitlist: 43 Number of computed successors: 9746 Max successors for one state: 2 Number of times merged: 1451 Number of times stopped: 1499 Number of times breaked: 1 Total time for CPA algorithm: 12.683s (Max: 11.748s) Time for choose from waitlist: 0.082s Time for precision adjustment: 8.000s Time for transfer relation: 2.689s Time for merge operator: 1.385s Time for stop operator: 0.112s Time for adding to reached set: 0.175s 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.069s Counterexample analysis: 0.028s (Max: 0.028s, Calls: 1) Refinement sat check: 0.022s Interpolant computation: 0.000s Error path post-processing: 0.000s Path-formulas extraction: 0.000s Building the counterexample trace: 0.028s 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.: 792 Max. size of reached set after ref.: 1 Avg. size of reached set before ref.: 792.00 Avg. size of reached set after ref.: 1.00 Total time for CEGAR algorithm: 12.764s Time for refinements: 0.081s Average time for refinement: 0.081s Max time for refinement: 0.081s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 0 CPAchecker general statistics ----------------------------- Number of program locations: 914 Number of functions: 31 Number of loops: 2 Size of reached set: 7457 Number of reached locations: 685 (75%) Avg states per location: 10 Max states per location: 82 (at node N22) Number of reached functions: 17 (55%) Number of partitions: 7457 Avg size of partitions: 1 Max size of partitions: 1 Number of target states: 0 Time for analysis setup: 4.887s Time for loading CPAs: 0.446s Time for loading parser: 0.721s Time for CFA construction: 3.674s Time for parsing file(s): 1.864s Time for AST to CFA: 1.251s Time for CFA sanity check: 0.000s Time for post-processing: 0.316s Time for var class.: 0.000s Time for Analysis: 12.774s CPU time for analysis: 12.770s Total time for CPAchecker: 17.661s Total CPU time for CPAchecker: 17.660s Time for Garbage Collector: 0.418s (in 5 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 572MB ( 545 MiB) max; 128MB ( 122 MiB) avg; 589MB ( 562 MiB) peak Used non-heap memory: 25MB ( 24 MiB) max; 21MB ( 20 MiB) avg; 25MB ( 24 MiB) peak Used in PS Old Gen pool: 37MB ( 35 MiB) max; 5MB ( 5 MiB) avg; 37MB ( 35 MiB) peak Allocated heap memory: 902MB ( 860 MiB) max; 607MB ( 579 MiB) avg Allocated non-heap memory: 26MB ( 25 MiB) max; 25MB ( 24 MiB) avg Total process virtual memory: 4899MB ( 4672 MiB) max; 4899MB ( 4672 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".