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.0/ALL.prp test/programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i -------------------------------------------------------------------------------- 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 6062: Dead code detected: __asm__ ("movb %%gs:%P1,%0": "=q" (pfo_ret__): "p" (& current_task)); (CFACreationUtils.addEdgeToCFA, INFO) line 6066: Dead code detected: __asm__ ("movw %%gs:%P1,%0": "=r" (pfo_ret__): "p" (& current_task)); (CFACreationUtils.addEdgeToCFA, INFO) line 6070: Dead code detected: __asm__ ("movl %%gs:%P1,%0": "=r" (pfo_ret__): "p" (& current_task)); (CFACreationUtils.addEdgeToCFA, INFO) line 6058: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 13317: Dead code detected: __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val), "c" (idle_mode): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 13321: Dead code detected: __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val), "c" (idle_mode): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 13330: Dead code detected: __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val), "c" (idle_mode): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 13313: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 13673: Dead code detected: __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (mask_ptr)); (CFACreationUtils.addEdgeToCFA, INFO) line 13677: Dead code detected: __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (mask_ptr)); (CFACreationUtils.addEdgeToCFA, INFO) line 13686: Dead code detected: __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (mask_ptr)); (CFACreationUtils.addEdgeToCFA, INFO) line 13669: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) line 13809: Dead code detected: tmp___6 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 13819: Dead code detected: tmp___7 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 13829: Dead code detected: tmp___8 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 13804: Dead code detected: Goto: switch_default___0 (CFACreationUtils.addEdgeToCFA, INFO) line 13905: Dead code detected: tmp___13 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 13915: Dead code detected: tmp___14 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 13925: Dead code detected: tmp___15 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 13900: Dead code detected: Goto: switch_default___1 (CFACreationUtils.addEdgeToCFA, INFO) line 14117: Dead code detected: tmp___26 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14127: Dead code detected: tmp___27 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14137: Dead code detected: tmp___28 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14112: Dead code detected: Goto: switch_default___2 (CFACreationUtils.addEdgeToCFA, INFO) lines 14213-14214: Dead code detected: __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val), "c" (mask_ptr): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) lines 14218-14219: Dead code detected: __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val), "c" (mask_ptr): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) lines 14229-14230: Dead code detected: __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val), "c" (mask_ptr): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14209: Dead code detected: Goto: switch_default___3 (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 14284: Dead code detected: __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val), "c" (if_mode): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14288: Dead code detected: __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val), "c" (if_mode): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14297: Dead code detected: __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val), "c" (if_mode): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14280: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 14398: Dead code detected: __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val), "c" (xsync): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14402: Dead code detected: __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val), "c" (xsync): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14411: Dead code detected: __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val), "c" (xsync): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14394: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 14497: Dead code detected: __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val), "c" (xctrl): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14501: Dead code detected: __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val), "c" (xctrl): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14510: Dead code detected: __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val), "c" (xctrl): "ebx"); (CFACreationUtils.addEdgeToCFA, INFO) line 14493: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 14738: Dead code detected: tmp = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14748: Dead code detected: tmp___0 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14758: Dead code detected: tmp___1 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14733: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 14831: Dead code detected: tmp = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14841: Dead code detected: tmp___0 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14851: Dead code detected: tmp___1 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 14826: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 15165: Dead code detected: tmp___1 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15175: Dead code detected: tmp___2 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15185: Dead code detected: tmp___3 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15160: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) line 15257: Dead code detected: tmp___8 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15267: Dead code detected: tmp___9 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15277: Dead code detected: tmp___10 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15252: Dead code detected: Goto: switch_default___0 (CFACreationUtils.addEdgeToCFA, INFO) line 15412: Dead code detected: tmp___12 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15422: Dead code detected: tmp___13 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15432: Dead code detected: tmp___14 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15407: Dead code detected: Goto: switch_default___1 (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) line 15813: Dead code detected: tmp___2 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15823: Dead code detected: tmp___3 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15833: Dead code detected: tmp___4 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15808: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) line 15956: Dead code detected: tmp___9 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15966: Dead code detected: tmp___10 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15976: Dead code detected: tmp___11 = get_current(); (CFACreationUtils.addEdgeToCFA, INFO) line 15951: Dead code detected: Goto: switch_default___0 (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Inline assembler ignored, analysis is probably unsound! (CFABuilder.createCFA, WARNING) line 6750: Function pointer *(ops__1->alloc_coherent) with type void * (*)(struct device *, size_t , dma_addr_t *, gfp_t ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 6805: Function pointer *(ops__1->free_coherent) with type void (*)(struct device *, size_t , void *, dma_addr_t ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 7240: Function pointer *(hdlc->proto->type_trans) with type __be16 (*)(struct sk_buff *, struct net_device *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) line 7683: Function pointer *(ld->ops->receive_buf) with type void (*)(struct tty_struct *, const unsigned char *, char *, 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 alloc_tty_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_set_operations to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_register_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __pci_register_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function put_tty_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_unregister_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function pci_unregister_driver to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function unregister_hdlc_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function free_netdev 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 6805: Ignoring function call through function pointer *(ops__1->free_coherent): (*(ops__1->free_coherent))(dev, size, vaddr, bus); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function free_irq to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __release_region 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 del_timer to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_unregister_device 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 _raw_spin_unlock to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function schedule_work 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 msecs_to_jiffies to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function mod_timer to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function netpoll_trap to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __netif_schedule to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function do_SAK to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function netif_carrier_on to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function netif_carrier_off to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_hangup to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_lock_irqsave 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 tty_wakeup 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 del_timer_sync 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 tty_get_baud_rate to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function jiffies_to_msecs to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function msleep_interruptible 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 memset to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __builtin_object_size to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Cannot get declaration of function __builtin_object_size, ignoring calls to it. (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) 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) Assuming external function __init_waitqueue_head 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 schedule to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function remove_wait_queue to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_port_close_start to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_ldisc_flush to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_port_close_end to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_hung_up_p to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_port_raise_dtr_rts to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_port_carrier_raised to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_unlock to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_lock to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function interruptible_sleep_on to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ldv_check_return_value to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function capable to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function hdlc_close to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ldv_undefined_int to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function hdlc_open to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function single_open 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_set_master to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __request_region to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ioremap_nocache to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 6750: Ignoring function call through function pointer *(ops__1->alloc_coherent): memory = (*(ops__1->alloc_coherent))(dev, size, dma_handle, tmp___1); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function debug_dma_alloc_coherent 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 memcmp to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tty_register_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function alloc_hdlcdev to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function register_netdev 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 tty_port_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __init_work to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function lockdep_init_map to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function init_timer_key to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Warning: Analysis stopped (The CPU-time limit of 900s has elapsed.) (ShutdownNotifier.shutdownIfNecessary, WARNING) PredicateCPA statistics ----------------------- Number of abstractions: 233472 (1% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 233472 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 868 (0%) Times precision was {false}: 0 (0%) Times result was cached: 216722 (93%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 15882 (7%) Times result was 'false': 2487 (1%) Number of strengthen sat checks: 161 Times result was 'false': 54 (34%) Number of coverage checks: 7304201 BDD entailment checks: 182607 Number of SMT sat checks: 161 trivial: 0 cached: 138 Max ABE block size: 288 Number of predicates discovered: 28 Number of abstraction locations: 25 Max number of predicates per location: 15 Avg number of predicates per location: 7 Total predicates per abstraction: 119487 Max number of predicates per abstraction: 14 Avg number of predicates per abstraction: 7.52 Number of irrelevant predicates: 20577 (17%) Number of preds handled by boolean abs: 98910 (83%) Total number of models for allsat: 137257 Max number of models for allsat: 52 Avg number of models for allsat: 8.64 Number of path formula cache hits: 24216995 (80%) Time for post operator: 37.745s Time for path formula creation: 32.879s Actual computation: 21.784s Time for strengthen operator: 7.100s Time for satisfiability checks: 0.025s Time for prec operator: 467.160s Time for abstraction: 464.891s (Max: 31.129s, Count: 233472) Boolean abstraction: 310.424s Solving time: 45.870s (Max: 23.391s) Model enumeration time: 261.102s Time for BDD construction: 0.846s (Max: 0.016s) Time for merge operator: 40.473s Time for coverage check: 0.465s Time for BDD entailment checks: 0.157s Total time for SMT solver (w/o itp): 306.996s Number of BDD nodes: 2973 Size of BDD node table: 10007 Size of BDD node cleanup queue: 21570 (count: 249501, min: 0, max: 818, avg: 0,09) Time for BDD node cleanup: 0.018s Time for BDD garbage collection: 0.028s (in 31 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: 38.429s Time for transition matches: 8.172s Time for transition assertions: 0.001s Time for transition actions: 0.000s Automaton transfers with branching: 0 Automaton transfer successors: 42518988 (count: 42518988, min: 1, max: 1, avg: 1,00) [1 x 42518988] CPA algorithm statistics ------------------------ Number of iterations: 23555947 Max size of waitlist: 2060 Average size of waitlist: 884 Number of computed successors: 27285744 Max successors for one state: 2 Number of times merged: 3560797 Number of times stopped: 3689167 Number of times breaked: 107 Total time for CPA algorithm: 817.992s (Max: 103.660s) Time for choose from waitlist: 2.525s Time for precision adjustment: 484.198s Time for transfer relation: 213.951s Time for merge operator: 58.216s Time for stop operator: 10.831s Time for adding to reached set: 22.662s Predicate-Abstraction Refiner statistics ---------------------------------------- Avg. length of target path (in blocks): 1518 (count: 107, min: 6, max: 22, avg: 14,19) Time for refinement: 78.090s Counterexample analysis: 38.927s (Max: 20.237s, Calls: 107) Refinement sat check: 1.257s Interpolant computation: 37.590s Error path post-processing: 0.000s Path-formulas extraction: 0.003s Building the counterexample trace: 38.927s Extracting precise counterexample: 0.000s Predicate creation: 0.005s Precision update: 0.031s ARG update: 38.725s Length of refined path (in blocks): 904 (count: 106, min: 2, max: 18, avg: 8,53) Number of affected states: 253 (count: 106, min: 1, max: 17, avg: 2,39) Length (states) of path with itp 'true': 545 (count: 106, min: 0, max: 8, avg: 5,14) Length (states) of path with itp non-trivial itp: 253 (count: 106, min: 1, max: 17, avg: 2,39) Length (states) of path with itp 'false': 106 (count: 106, min: 1, max: 1, avg: 1,00) Different non-trivial interpolants along paths: 30 (count: 106, min: 0, max: 5, avg: 0,28) Equal non-trivial interpolants along paths: 117 (count: 106, min: 0, max: 14, avg: 1,10) 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: 107 Number of successful refinements: 107 Number of failed refinements: 0 Max. size of reached set before ref.: 1192171 Max. size of reached set after ref.: 660069 Avg. size of reached set before ref.: 683741.23 Avg. size of reached set after ref.: 469658.75 Total time for CEGAR algorithm: 896.158s Time for refinements: 78.163s Average time for refinement: 0.730s Max time for refinement: 20.445s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 0 CPAchecker general statistics ----------------------------- Number of program locations: 4986 Number of functions: 206 Number of loops: 55 Size of reached set: 689751 Number of reached locations: 4301 (86%) Avg states per location: 160 Max states per location: 12097 (at node N161) Number of reached functions: 179 (87%) Number of partitions: 689639 Avg size of partitions: 1 Max size of partitions: 8 (with key [N3410 (before lines 12594-12600), Function slgt_interrupt called from node N8316, stack depth 2 [14ff80ba], stack [main, slgt_interrupt], Init]) Number of target states: 0 Size of final wait list 1166 Time for analysis setup: 5.507s Time for loading CPAs: 0.672s Time for loading parser: 0.408s Time for CFA construction: 4.391s Time for parsing file(s): 1.327s Time for AST to CFA: 1.983s Time for CFA sanity check: 0.000s Time for post-processing: 0.776s Time for var class.: 0.000s Time for Analysis: 896.158s CPU time for analysis: 895.960s Total time for CPAchecker: 901.666s Total CPU time for CPAchecker: 901.470s Time for Garbage Collector: 472.326s (in 466 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 2853MB ( 2721 MiB) max; 1770MB ( 1688 MiB) avg; 3335MB ( 3180 MiB) peak Used non-heap memory: 29MB ( 28 MiB) max; 26MB ( 25 MiB) avg; 29MB ( 28 MiB) peak Used in PS Old Gen pool: 2097MB ( 1999 MiB) max; 1376MB ( 1312 MiB) avg; 2097MB ( 1999 MiB) peak Allocated heap memory: 3047MB ( 2906 MiB) max; 2619MB ( 2498 MiB) avg Allocated non-heap memory: 54MB ( 51 MiB) max; 39MB ( 37 MiB) avg Total process virtual memory: 4900MB ( 4673 MiB) max; 4899MB ( 4672 MiB) avg Verification result: UNKNOWN, incomplete analysis. More details about the verification run can be found in the directory "./output".