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--media--dvb--ttpci--budget.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 13895: Function pointer *__a___13 with type struct dvb_frontend * (*)(const struct stv090x_config *, struct i2c_adapter *, enum stv090x_demodulator ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13980: Function pointer *__a___14 with type struct stv6110x_devctl * (*)(struct dvb_frontend *, const struct stv6110x_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 14192: Function pointer *__a___15 with type struct dvb_frontend * (*)(struct dvb_frontend *, struct i2c_adapter *, const struct isl6423_config *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13603: Function pointer *__a___10 with type struct dvb_frontend * (*)(const struct tda10086_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13686: Function pointer *__a___11 with type struct dvb_frontend * (*)(struct dvb_frontend *, int, struct i2c_adapter *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13777: Function pointer *__a___12 with type struct dvb_frontend * (*)(struct dvb_frontend *, struct i2c_adapter *, u8 , u8 ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13384: Function pointer *__a___8 with type struct dvb_frontend * (*)(const struct s5h1420_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13487: Function pointer *__a___9 with type struct dvb_frontend * (*)(struct dvb_frontend *, struct i2c_adapter *, u8 , u8 ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13271: Function pointer *__a___7 with type struct dvb_frontend * (*)(const struct l64781_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13152: Function pointer *__a___6 with type struct dvb_frontend * (*)(const struct tda1004x_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 13019: Function pointer *__a___5 with type struct dvb_frontend * (*)(const struct tda8083_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12862: Function pointer *__a___4 with type struct dvb_frontend * (*)(const struct stv0299_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12683: Function pointer *__a___3 with type struct dvb_frontend * (*)(const struct stv0299_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12542: Function pointer *__a___2 with type struct dvb_frontend * (*)(const struct l64781_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12439: Function pointer *__a___1 with type struct dvb_frontend * (*)(const struct ves1820_config *, struct i2c_adapter *, u8 ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12093: Function pointer *__a with type struct dvb_frontend * (*)(const struct ves1x93_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 12235: Function pointer *__a___0 with type struct dvb_frontend * (*)(const struct stv0299_config *, struct i2c_adapter *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 7894: Function pointer *__cil_tmp16 with type int (*)(struct dvb_frontend *, const u8 *, 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) Assuming external function saa7146_register_extension 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 ttpci_budget_init 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 13384: Ignoring call via function pointer frontend_init::__a___8 for which no suitable target was found in line: tmp___58 = (*__a___8)(__cil_tmp449, __cil_tmp452); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13384: Ignoring function call through function pointer *__a___8: tmp___58 = (*__a___8)(__cil_tmp449, __cil_tmp452); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __symbol_put to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 13487: Ignoring call via function pointer frontend_init::__a___9 for which no suitable target was found in line: tmp___63 = (*__a___9)(__cil_tmp470, __cil_tmp473, __cil_tmp474, __cil_tmp475); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13487: Ignoring function call through function pointer *__a___9: tmp___63 = (*__a___9)(__cil_tmp470, __cil_tmp473, __cil_tmp474, __cil_tmp475); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function saa7146_setgpio to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function msleep to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 13603: Ignoring call via function pointer frontend_init::__a___10 for which no suitable target was found in line: tmp___68 = (*__a___10)(__cil_tmp491, __cil_tmp494); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13603: Ignoring function call through function pointer *__a___10: tmp___68 = (*__a___10)(__cil_tmp491, __cil_tmp494); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13686: Ignoring call via function pointer frontend_init::__a___11 for which no suitable target was found in line: tmp___73 = (*__a___11)(__cil_tmp505, 96, __cil_tmp508, 0); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13686: Ignoring function call through function pointer *__a___11: tmp___73 = (*__a___11)(__cil_tmp505, 96, __cil_tmp508, 0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13777: Ignoring call via function pointer frontend_init::__a___12 for which no suitable target was found in line: tmp___78 = (*__a___12)(__cil_tmp518, __cil_tmp521, __cil_tmp522, __cil_tmp523); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13777: Ignoring function call through function pointer *__a___12: tmp___78 = (*__a___12)(__cil_tmp518, __cil_tmp521, __cil_tmp522, __cil_tmp523); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13895: Ignoring call via function pointer frontend_init::__a___13 for which no suitable target was found in line: tmp___83 = (*__a___13)(__cil_tmp539, __cil_tmp542, __cil_tmp543); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13895: Ignoring function call through function pointer *__a___13: tmp___83 = (*__a___13)(__cil_tmp539, __cil_tmp542, __cil_tmp543); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13980: Ignoring call via function pointer frontend_init::__a___14 for which no suitable target was found in line: tmp___88 = (*__a___14)(__cil_tmp554, __cil_tmp555, __cil_tmp558); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13980: Ignoring function call through function pointer *__a___14: tmp___88 = (*__a___14)(__cil_tmp554, __cil_tmp555, __cil_tmp558); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 14141: Ignoring call via function pointer frontend_init::__cil_tmp605 for which no suitable target was found in line: (*__cil_tmp605)(__cil_tmp608); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 14141: Ignoring function call through function pointer *__cil_tmp605: (*__cil_tmp605)(__cil_tmp608); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 10683: Ignoring call via function pointer grundig_29504_451_tuner_set_params::__cil_tmp42 for which no suitable target was found in line: (*__cil_tmp42)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 10683: Ignoring function call through function pointer *__cil_tmp42: (*__cil_tmp42)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __const_udelay 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 i2c_transfer to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 10164: Ignoring call via function pointer alps_tdbe2_tuner_set_params::__cil_tmp56 for which no suitable target was found in line: (*__cil_tmp56)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 10164: Ignoring function call through function pointer *__cil_tmp56: (*__cil_tmp56)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 9932: Ignoring call via function pointer alps_bsrv2_tuner_set_params::__cil_tmp65 for which no suitable target was found in line: (*__cil_tmp65)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 9932: Ignoring function call through function pointer *__cil_tmp65: (*__cil_tmp65)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 8575: Ignoring call via function pointer alps_bsbe1_tuner_set_params::__cil_tmp50 for which no suitable target was found in line: (*__cil_tmp50)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 8575: Ignoring function call through function pointer *__cil_tmp50: (*__cil_tmp50)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 8857: Ignoring call via function pointer alps_tdhd1_204a_tuner_set_params::__cil_tmp62 for which no suitable target was found in line: (*__cil_tmp62)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 8857: Ignoring function call through function pointer *__cil_tmp62: (*__cil_tmp62)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 10505: Ignoring call via function pointer grundig_29504_401_tuner_set_params::__cil_tmp79 for which no suitable target was found in line: (*__cil_tmp79)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 10505: Ignoring function call through function pointer *__cil_tmp79: (*__cil_tmp79)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 10891: Ignoring call via function pointer s5h1420_tuner_set_params::__cil_tmp48 for which no suitable target was found in line: (*__cil_tmp48)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 10891: Ignoring function call through function pointer *__cil_tmp48: (*__cil_tmp48)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 8245: Ignoring call via function pointer alps_bsru6_tuner_set_params::__cil_tmp55 for which no suitable target was found in line: (*__cil_tmp55)(fe, 1); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 8245: Ignoring function call through function pointer *__cil_tmp55: (*__cil_tmp55)(fe, 1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 14192: Ignoring call via function pointer frontend_init::__a___15 for which no suitable target was found in line: tmp___93 = (*__a___15)(__cil_tmp612, __cil_tmp615, __cil_tmp616); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 14192: Ignoring function call through function pointer *__a___15: tmp___93 = (*__a___15)(__cil_tmp612, __cil_tmp615, __cil_tmp616); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13271: Ignoring call via function pointer frontend_init::__a___7 for which no suitable target was found in line: tmp___53 = (*__a___7)(__cil_tmp425, __cil_tmp428); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13271: Ignoring function call through function pointer *__a___7: tmp___53 = (*__a___7)(__cil_tmp425, __cil_tmp428); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13152: Ignoring call via function pointer frontend_init::__a___6 for which no suitable target was found in line: tmp___48 = (*__a___6)(__cil_tmp398, __cil_tmp401); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13152: Ignoring function call through function pointer *__a___6: tmp___48 = (*__a___6)(__cil_tmp398, __cil_tmp401); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 13019: Ignoring call via function pointer frontend_init::__a___5 for which no suitable target was found in line: tmp___43 = (*__a___5)(__cil_tmp366, __cil_tmp369); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 13019: Ignoring function call through function pointer *__a___5: tmp___43 = (*__a___5)(__cil_tmp366, __cil_tmp369); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12862: Ignoring call via function pointer frontend_init::__a___4 for which no suitable target was found in line: tmp___38 = (*__a___4)(__cil_tmp326, __cil_tmp329); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12862: Ignoring function call through function pointer *__a___4: tmp___38 = (*__a___4)(__cil_tmp326, __cil_tmp329); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12683: Ignoring call via function pointer frontend_init::__a___3 for which no suitable target was found in line: tmp___33 = (*__a___3)(__cil_tmp278, __cil_tmp281); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12683: Ignoring function call through function pointer *__a___3: tmp___33 = (*__a___3)(__cil_tmp278, __cil_tmp281); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12542: Ignoring call via function pointer frontend_init::__a___2 for which no suitable target was found in line: tmp___27 = (*__a___2)(__cil_tmp249, __cil_tmp252); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12542: Ignoring function call through function pointer *__a___2: tmp___27 = (*__a___2)(__cil_tmp249, __cil_tmp252); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12439: Ignoring call via function pointer frontend_init::__a___1 for which no suitable target was found in line: tmp___22 = (*__a___1)(__cil_tmp230, __cil_tmp233, tmp___21); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12439: Ignoring function call through function pointer *__a___1: tmp___22 = (*__a___1)(__cil_tmp230, __cil_tmp233, tmp___21); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12093: Ignoring call via function pointer frontend_init::__a for which no suitable target was found in line: tmp___11 = (*__a)(__cil_tmp136, __cil_tmp139); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12093: Ignoring function call through function pointer *__a: tmp___11 = (*__a)(__cil_tmp136, __cil_tmp139); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) line 12235: Ignoring call via function pointer frontend_init::__a___0 for which no suitable target was found in line: tmp___16 = (*__a___0)(__cil_tmp173, __cil_tmp176); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 12235: Ignoring function call through function pointer *__a___0: tmp___16 = (*__a___0)(__cil_tmp173, __cil_tmp176); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function dvb_register_frontend to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ttpci_budget_init_hooks to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function saa7146_unregister_extension to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Stopping analysis ... (CPAchecker.runAlgorithm, INFO) PredicateCPA statistics ----------------------- Number of abstractions: 244 (2% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 244 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 122 (50%) Times precision was {false}: 0 (0%) Times result was cached: 78 (32%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 44 (18%) Times result was 'false': 0 (0%) Number of strengthen sat checks: 4 Times result was 'false': 3 (75%) Number of coverage checks: 2278 BDD entailment checks: 146 Number of SMT sat checks: 4 trivial: 0 cached: 1 Max ABE block size: 171 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: 88 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: 88 (100%) Total number of models for allsat: 44 Max number of models for allsat: 1 Avg number of models for allsat: 1.00 Number of path formula cache hits: 6024 (53%) Time for post operator: 0.739s Time for path formula creation: 0.658s Actual computation: 0.621s Time for strengthen operator: 0.049s Time for satisfiability checks: 0.024s Time for prec operator: 2.694s Time for abstraction: 2.676s (Max: 0.891s, Count: 244) Boolean abstraction: 1.197s Solving time: 1.099s (Max: 0.447s) Model enumeration time: 0.081s Time for BDD construction: 0.001s (Max: 0.001s) Time for merge operator: 1.835s Time for coverage check: 0.003s Time for BDD entailment checks: 0.001s Total time for SMT solver (w/o itp): 1.204s Number of BDD nodes: 203 Size of BDD node table: 10007 Size of BDD node cleanup queue: 24 (count: 451, min: 0, max: 24, avg: 0,05) 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.164s Automaton transfers with branching: 0 Automaton transfer successors: 27283 (count: 27283, min: 1, max: 1, avg: 1,00) [1 x 27283] CPA algorithm statistics ------------------------ Number of iterations: 9527 Max size of waitlist: 105 Average size of waitlist: 46 Number of computed successors: 10740 Max successors for one state: 2 Number of times merged: 1066 Number of times stopped: 1212 Number of times breaked: 1 Total time for CPA algorithm: 6.322s (Max: 3.610s) Time for choose from waitlist: 0.050s Time for precision adjustment: 2.800s Time for transfer relation: 1.270s Time for merge operator: 1.908s Time for stop operator: 0.047s Time for adding to reached set: 0.065s 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.084s Counterexample analysis: 0.013s (Max: 0.013s, Calls: 1) Refinement sat check: 0.010s Interpolant computation: 0.000s Error path post-processing: 0.000s Path-formulas extraction: 0.000s Building the counterexample trace: 0.013s 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.: 4763 Max. size of reached set after ref.: 1 Avg. size of reached set before ref.: 4763.00 Avg. size of reached set after ref.: 1.00 Total time for CEGAR algorithm: 6.416s Time for refinements: 0.093s Average time for refinement: 0.093s Max time for refinement: 0.093s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 0 CPAchecker general statistics ----------------------------- Number of program locations: 1249 Number of functions: 41 Number of loops: 6 Size of reached set: 4767 Number of reached locations: 1103 (88%) Avg states per location: 4 Max states per location: 32 (at node N646) Number of reached functions: 27 (66%) Number of partitions: 4767 Avg size of partitions: 1 Max size of partitions: 1 Number of target states: 0 Time for analysis setup: 4.000s Time for loading CPAs: 1.011s Time for loading parser: 0.348s Time for CFA construction: 2.528s Time for parsing file(s): 0.846s Time for AST to CFA: 1.057s Time for CFA sanity check: 0.000s Time for post-processing: 0.473s Time for var class.: 0.000s Time for Analysis: 6.422s CPU time for analysis: 15.430s Total time for CPAchecker: 10.424s Total CPU time for CPAchecker: 21.750s Time for Garbage Collector: 0.164s (in 4 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 576MB ( 549 MiB) max; 283MB ( 270 MiB) avg; 579MB ( 552 MiB) peak Used non-heap memory: 26MB ( 24 MiB) max; 20MB ( 19 MiB) avg; 26MB ( 25 MiB) peak Used in PS Old Gen pool: 0MB ( 0 MiB) max; 0MB ( 0 MiB) avg; 0MB ( 0 MiB) peak Allocated heap memory: 2553MB ( 2435 MiB) max; 2105MB ( 2008 MiB) avg Allocated non-heap memory: 27MB ( 25 MiB) max; 24MB ( 23 MiB) avg Total process virtual memory: 57054MB ( 54411 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".