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/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.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) lines 7771-7795: Dead code detected: __asm__ volatile ("" "771:\n\t" "call *%c[paravirt_opptr];" "\n" "772:\n" ".pushsection .parainstructions,\"a\"\n" " " ".balign 8" " " "\n" " " ".quad" " " " 771b\n" " .byte " "%c[paravirt_typenum]" "\n" " .byte 772b-771b\n" " .short " "%c[paravirt_clobber]" "\n" ".popsection\n" "": "=a" (__eax): [paravirt_typenum] "i" ((unsigned long )((unsigned int )(& ((struct paravirt_patch_template *)0)->pv_irq_ops.save_fl.func)) / sizeof(void *)), [paravirt_opptr] "i" (& pv_irq_ops.save_fl.func), [paravirt_clobber] "i" (1): "memory", "cc"); (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label while_break is not reachable. (CFAFunctionBuilder.leave, INFO) line 11195: Dead code detected: Goto: switch_break (CFACreationUtils.addEdgeToCFA, INFO) line 11204: Dead code detected: Goto: switch_break (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO) line 11348: Dead code detected: Goto: switch_break (CFACreationUtils.addEdgeToCFA, INFO) line 11357: Dead code detected: Goto: switch_break (CFACreationUtils.addEdgeToCFA, INFO) line 12253: Dead code detected: Goto: switch_break (CFACreationUtils.addEdgeToCFA, INFO) line 13358: Dead code detected: Goto: while_break (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label while_break is not reachable. (CFAFunctionBuilder.leave, INFO) line 13443: Dead code detected: Goto: while_break (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label while_break is not reachable. (CFAFunctionBuilder.leave, INFO) Inline assembler ignored, analysis is probably unsound! (CFABuilder.createCFA, WARNING) line 8098: Function pointer *(ops->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 8176: Function pointer *(ops->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) lines 9178-9180: Function pointer *(dec->audio_filter->feed->cb.ts) with type int (*)(const u8 *, size_t , const u8 *, size_t , struct dmx_ts_feed *, enum dmx_success ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) lines 9632-9634: Function pointer *(filter->feed->cb.sec) with type int (*)(const u8 *, size_t , const u8 *, size_t , struct dmx_section_filter *, enum dmx_success ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) lines 9519-9522: Function pointer *(dec->audio_filter->feed->cb.ts) with type int (*)(const u8 *, size_t , const u8 *, size_t , struct dmx_ts_feed *, enum dmx_success ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) lines 9389-9392: Function pointer *(dec->video_filter->feed->cb.ts) with type int (*)(const u8 *, size_t , const u8 *, size_t , struct dmx_ts_feed *, enum dmx_success ) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) lines 9195-9197: Function pointer *(dec->video_filter->feed->cb.ts) with type int (*)(const u8 *, size_t , const u8 *, size_t , struct dmx_ts_feed *, enum dmx_success ) 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 usb_register_driver 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 dev_set_drvdata to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function tasklet_kill to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function list_del to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_kill_urb to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function input_unregister_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 8176: Ignoring function call through function pointer *(ops->free_coherent): (*(ops->free_coherent))(dev, size, vaddr, bus); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function __mutex_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function ldv_undefined_pointer to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 8098: Ignoring function call through function pointer *(ops->alloc_coherent): memory = (*(ops->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 memset to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7990eca6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@29fd9f9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6e448bd0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@23e7cde4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6e49c8f1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@43f66bae: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@69d8e38c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@750aacb1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@f0d1c1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@cad055d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5a815e0c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@722fd5ba: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7b232c7c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5ef21bc4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1913d82c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@54c27943: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4946ed22: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@24147818: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@42f00500: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5ca83ed0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Infeasible counterexample found, but could not remove it from the ARG. Therefore, we cannot prove safety. (CounterexampleCheckAlgorithm.checkCounterexample, WARNING) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@14bccf7f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1dacc690: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3341afc6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@28f890ac: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5a831414: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@448d0b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@782256a2: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@77ddf857: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5538a5d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@35097440: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7e1fa11d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@69761a56: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@67c215c8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@190728ba: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@211d9167: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@f770b88: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6563985e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5ca92583: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@8cb7e08: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@60cea70d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Assuming external function mutex_lock_interruptible_nested to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function usb_bulk_msg 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 request_firmware to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function crc32_le to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function release_firmware to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@19349cc1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@12b43ee9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@34ef2a9a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@173d1008: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6597e5d0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5eef3d7b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@475137e1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@660b5b7e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@30c723e8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1a6ed38d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5fd857ab: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5e7e7944: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4476823b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@c0e6e36: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7604790c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@66c9f0e7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1e2639: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7c0972fa: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@59d04f4c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@73cd8020: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58ad6934: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@85fc923: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3a771634: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@125e3283: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@463684dc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2e11e512: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5433e756: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@68b61f16: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@63108d38: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@78abda9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5834b7ab: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@202a1832: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@53eebefb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6dfb2773: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@62dee8b8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2cce366d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3d5f5474: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@34bfbc0f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@e932de: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4d34aec3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3a4f293e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@34820291: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2538f7f5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5cdcc3b8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@797edeb7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@66cc70d7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2fa77283: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@28e4262d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@19ce8f40: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@32b21adc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7c4a754a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@496ed82e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5b01522c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@10b04117: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@76767319: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6856659: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@a852294: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@278b89e8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@33b526df: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@478c0785: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5f9e1fb6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@762c7512: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1d3afee7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2c8bb015: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@36b8994b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@423b8b54: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2d1a8f13: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7e38a2e5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3a8fd670: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@64bf2596: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4dd2c7f5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4e388b0c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@341f8fa5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4d921f43: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@150ea328: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2fd37de7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@406555ec: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6acc808e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58fc2912: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@c68740c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4cd72139: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@35706368: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@46de2fbc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5dfddf46: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@72c76b65: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6b140dfc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@745734c5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@51f7cfbe: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7fc60c00: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4004d964: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@17708fcb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@40badc7b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@55bdbd6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@9327f19: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1e2496ae: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3d2df592: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@20d97acd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58091fbf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2dd67838: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@34da19b8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5fea7164: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58c660ac: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5d98941f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7d28ecc8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@405772e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@69e503f7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6eda0568: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@44c36d6d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@29d97884: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4d122601: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@a88b4d0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@49efec44: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@e27125: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@53f1fe88: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@500e7c64: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5e95cfbd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@a0f3f53: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6843ed14: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@619f4d36: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@65966cb4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3531b3c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5f00d689: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4b573f89: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@404731cc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@31ad810b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@387824c4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5d24bb5d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@48dd3166: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3113387e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@24704ae1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@55ad9997: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@39f43fe8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1841ef12: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7d15be47: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1bb2e2c8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@297da553: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2a9d77f4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2c26e3da: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@8a4ab68: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@19119096: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@66985cbb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@37586486: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58961938: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@51821294: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@8c7bc44: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4a6a14f4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1d3b7a34: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@29558b15: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@413f7f43: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@302db95a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6913c9bf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@53e7a6a9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@515a7e03: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@27a94855: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@68881cf4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5947911d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@129bfa97: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2c275c8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@467ee8f3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2356202e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1beb87ca: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@641569ef: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1d2b54a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@235a2a57: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7ccda7bc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2568a68d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@ee68f61: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@16344eaa: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@43a4b1c6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3693ba0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@55bc9896: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1b6baa68: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@32d8f6eb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@622ba41f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@14e45916: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@42c5461c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@50aafc04: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3905f6f3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@577d6271: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4638b008: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@39f9cf59: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4db4a0fb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4b952cfb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@31e427b1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3b2b863e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2737b902: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2669160a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@416b2ecc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@45023585: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@35b23fda: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@48f07732: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@27fb943: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5bf67108: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@60980daa: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6fb0398f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1d64b1fe: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5bed25d0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@292935cd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5523a13e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6207b64c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@792b3645: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3b3efe72: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@22d7f829: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5f5de42f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@385e7d9e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6e548a6a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5c9e7ffb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6fb8f88a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@9929a9a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6ec00b1a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5eba0b16: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@65d1f6a1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@591ac8a6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7797f968: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@404d0415: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6f8e377b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@13247bb8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2d85efce: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1f108a1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1a89dbcc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@cab9753: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6bd0726c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2363e28f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@60757610: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@64242fb5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@61ffc843: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@512242b9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1c04d55e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@78fc3f89: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@51a6b686: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6f904a0d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3961ac6b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@20c0ac7e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@571164e5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2ba1e4e9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4114da1c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1795f720: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@75c1bcc6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1964cc4f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@ebbbb3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@45551f96: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3323bb54: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5cbef89d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5756ffe7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@49cc6a78: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@72100465: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@79775887: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@498dcb1f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@cd3b719: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3b2659ec: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@42aeb1c8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1a50e179: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3ca633aa: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@59dcc6af: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2f014f8d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5f404a16: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7dfdabab: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@593539ef: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@557173c6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@32bc091d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4342c73a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@31411f11: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@658ec3b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@65c24409: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@573e83ca: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1832afbb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1fb4f53e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3c6f9c20: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@207ec1d2: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@f36479: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@dbc5a8b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2a25f71e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@317326da: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@40f6638: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@419b3168: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@14a2f562: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1430dc25: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@17a6e001: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@34d437b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2cd41185: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2a3b3093: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1962193b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5b0aa27e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6b8df395: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@673bbff8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@c95b534: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@557050dd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1f5bf5e9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@17e63276: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@11d546e1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1584e9f3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1eaca937: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@741feca2: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4ea153ac: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@14d59dd9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6ea83eff: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@23b2e42e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@c10fd00: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@e52cfb9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@200d05bf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6f732c85: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3900e3ee: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6c46203e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@b22645: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@b85bd90: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2074dadc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@9c9b1a3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58f9816d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6c375a23: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@31d2e3bd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5e587d31: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@311db79a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@72b78769: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4cd624db: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@127de1bf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1cfaed75: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@111b10f1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2e2442cd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@401b0510: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@13b3f4f6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3611556f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1968cf2c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5130ba78: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@603c4a3c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@473943c6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7d28371: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6ae2d7de: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4095ed1d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@77216dd1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4cf69ea9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@662cd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6d2459c4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@41767b91: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@33f3c32e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4c7dd84: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1aaf2efb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@34b81879: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3be26f19: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@52d9051: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3a110a52: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3ee6fb4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@43e36481: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@15b7db9c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@482f30e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2d766e65: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@217e3d20: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@249271a7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@d80c717: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1897af1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3fb82615: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5d18a6a8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2895f40d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@13e61c2d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@228777b8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6c401f89: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@50a3fc8f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@65af263e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@fefa219: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5a11efe: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@16bb3edf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@68bd5c1b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@751f73d6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6e2d5e1a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7b67d9b8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@54f28565: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6119c076: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@13715bd4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4c31091: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@29cbda50: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@243fa7c0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@60b69f84: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@33c766ac: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@28f41a9c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@37d4ff72: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@35720462: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2357ad85: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3449446c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@735b153: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5262041c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@687d9ddb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@41fc9076: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@385905ec: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@48d71b6e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@56f7c93d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2b6e4ea1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4f4cf214: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4763eef6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4af8a6f2: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@48d6f417: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1b87c3fa: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@23186854: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@481e408b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@50d5d796: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5008682a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@55936169: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1ff5ad3e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@419503bd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3351b95: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4c53c41d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4e834dce: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5372b3c2: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@92c560: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@74f3efa0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@59fbfddd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@38d1c86b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@66b97033: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7c1ed3d6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7d68bece: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@66ab1415: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@26b4208e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7059a5fb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@350c8a04: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7292ef6e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3ec07736: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@22a63e46: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1f0eeec1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@64d60bab: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@9a8107a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@796a7ef7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7c6f31e3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@62919012: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@66a10efc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@811c726: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@68f19c7a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@40b62baf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@70ca9f0a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@47c1ae13: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4fa262d5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7b8eabf: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@46f74da1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3fd5d407: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@30451d5b: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@10a13ef0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@e9a4637: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7f09fec3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@209eb750: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@14e64567: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@718acea: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2bfc52d5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5c30536f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@45f6c6bb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2b19cd8d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@61af3bef: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1a9da661: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@69fbe839: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7f23cdef: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@69d3526e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@63156f40: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4891ebb2: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7e2072f0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5ef66f3e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(hwdev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6a28a111: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@353aca20: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7ef17a89: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@13566aff: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(urb) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@48471cb6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2aec7dc9: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@52e1ca27: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(intf) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3d87b646: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dec) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@622047db: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Assuming external function dvb_register_adapter 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 12365: Ignoring function call through function pointer *(dec->demux.dmx.add_frontend): result = (*(dec->demux.dmx.add_frontend))(&(dec->demux.dmx), &(dec->frontend)); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) lines 9195-9197: Ignoring function call through function pointer *(dec->video_filter->feed->cb.ts): (*(dec->video_filter->feed->cb.ts))((const u8 *)data, (size_t )188, (const u8 *)((void *)0), (size_t )0, &(dec->video_filter->feed->feed.ts), (enum dmx_success )0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) lines 9178-9180: Ignoring function call through function pointer *(dec->audio_filter->feed->cb.ts): (*(dec->audio_filter->feed->cb.ts))((const u8 *)data, (size_t )188, (const u8 *)((void *)0), (size_t )0, &(dec->audio_filter->feed->feed.ts), (enum dmx_success )0); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Recursion detected, aborting. To ignore recursion, add -skipRecursion to the command line. (CallstackCPA:CallstackTransferRelation.getAbstractSuccessorsForEdge, INFO) Error: line 12365: Unsupported C feature (recursion): result = ttusb_dec_probe(&(dec->demux.dmx), &(dec->frontend)); (line was originally pointer call(ttusb_dec_probe) result = (*(dec->demux.dmx.add_frontend))(& dec->demux.dmx, & dec->frontend);) (CallstackTransferRelation.getAbstractSuccessorsForEdge, SEVERE) PredicateCPA statistics ----------------------- Number of abstractions: 2312 (2% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 2312 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 5 (0%) Times precision was {false}: 0 (0%) Times result was cached: 1136 (49%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 1171 (51%) Times result was 'false': 1024 (44%) Number of strengthen sat checks: 103 Times result was 'false': 51 (50%) Number of coverage checks: 23259 BDD entailment checks: 2771 Number of SMT sat checks: 103 trivial: 0 cached: 64 Max ABE block size: 250 Number of predicates discovered: 69 Number of abstraction locations: 12 Max number of predicates per location: 27 Avg number of predicates per location: 13 Total predicates per abstraction: 12616 Max number of predicates per abstraction: 27 Avg number of predicates per abstraction: 10.77 Number of irrelevant predicates: 561 (4%) Number of preds handled by boolean abs: 12055 (96%) Total number of models for allsat: 1133 Max number of models for allsat: 15 Avg number of models for allsat: 0.97 Number of path formula cache hits: 103847 (77%) Time for post operator: 2.990s Time for path formula creation: 2.645s Actual computation: 2.483s Time for strengthen operator: 0.255s Time for satisfiability checks: 0.152s Time for prec operator: 7.233s Time for abstraction: 7.198s (Max: 0.280s, Count: 2312) Boolean abstraction: 2.511s Solving time: 1.205s (Max: 0.115s) Model enumeration time: 0.357s Time for BDD construction: 0.197s (Max: 0.016s) Time for merge operator: 0.772s Time for coverage check: 0.075s Time for BDD entailment checks: 0.058s Total time for SMT solver (w/o itp): 1.712s Number of BDD nodes: 9736 Size of BDD node table: 10007 Size of BDD node cleanup queue: 10695 (count: 13989, min: 0, max: 5355, avg: 0,76) Time for BDD node cleanup: 0.007s Time for BDD garbage collection: 0.009s (in 1 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.545s Time for transition matches: 0.394s Time for transition assertions: 0.001s Time for transition actions: 0.000s Automaton transfers with branching: 0 Automaton transfer successors: 140400 (count: 140400, min: 1, max: 1, avg: 1,00) [1 x 140400] CPA algorithm statistics ------------------------ Number of iterations: 79947 Max size of waitlist: 131 Average size of waitlist: 29 Number of computed successors: 91862 Max successors for one state: 2 Number of times merged: 10244 Number of times stopped: 10824 Number of times breaked: 52 Total time for CPA algorithm: 15.361s (Max: 3.377s) Time for choose from waitlist: 0.118s Time for precision adjustment: 7.530s Time for transfer relation: 5.094s Time for merge operator: 1.288s Time for stop operator: 0.388s Time for adding to reached set: 0.318s Predicate-Abstraction Refiner statistics ---------------------------------------- Avg. length of target path (in blocks): 680 (count: 52, min: 4, max: 48, avg: 13,08) Time for refinement: 10.622s Counterexample analysis: 6.290s (Max: 0.879s, Calls: 52) Refinement sat check: 1.780s Interpolant computation: 3.723s Error path post-processing: 3.763s Path-formulas extraction: 0.000s Building the counterexample trace: 6.290s Extracting precise counterexample: 3.764s Predicate creation: 0.034s Precision update: 0.017s ARG update: 0.481s Length of refined path (in blocks): 446 (count: 26, min: 2, max: 48, avg: 17,15) Number of affected states: 404 (count: 26, min: 1, max: 46, avg: 15,54) Length (states) of path with itp 'true': 16 (count: 26, min: 0, max: 1, avg: 0,62) Length (states) of path with itp non-trivial itp: 404 (count: 26, min: 1, max: 46, avg: 15,54) Length (states) of path with itp 'false': 20 (count: 26, min: 0, max: 1, avg: 0,77) Different non-trivial interpolants along paths: 105 (count: 26, min: 0, max: 11, avg: 4,04) Equal non-trivial interpolants along paths: 273 (count: 26, min: 0, max: 37, avg: 10,50) 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: 52 Number of successful refinements: 27 Number of failed refinements: 0 Max. size of reached set before ref.: 6616 Max. size of reached set after ref.: 669 Avg. size of reached set before ref.: 2053.21 Avg. size of reached set after ref.: 403.37 Total time for CEGAR algorithm: 26.072s Time for refinements: 10.710s Average time for refinement: 0.205s Max time for refinement: 0.980s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 25 Number of infeasible paths: 25 (100%) Time for counterexample checks: 11.391s CPAchecker general statistics ----------------------------- Number of program locations: 1824 Number of functions: 86 Number of loops: 22 Size of reached set: 5256 Number of reached locations: 739 (41%) Avg states per location: 7 Max states per location: 36 (at node N1918) Number of reached functions: 45 (52%) Number of partitions: 5201 Avg size of partitions: 1 Max size of partitions: 20 (with key [N1346 (before lines 10384-10401), Function ttusb_dec_setup_urbs called from node N1971, stack depth 5 [170abfb4], stack [main, ttusb_dec_probe, ttusb_dec_init_usb, ttusb_dec_alloc_iso_urbs, ttusb_dec_setup_urbs], Init]) Number of target states: 0 Size of final wait list 43 Time for analysis setup: 4.872s Time for loading CPAs: 0.602s Time for loading parser: 0.697s Time for CFA construction: 3.502s Time for parsing file(s): 1.549s Time for AST to CFA: 1.226s Time for CFA sanity check: 0.000s Time for post-processing: 0.345s Time for var class.: 0.000s Time for Analysis: 37.464s CPU time for analysis: 37.460s Total time for CPAchecker: 42.337s Total CPU time for CPAchecker: 42.330s Time for Garbage Collector: 1.397s (in 8 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 1087MB ( 1037 MiB) max; 307MB ( 293 MiB) avg; 1140MB ( 1087 MiB) peak Used non-heap memory: 32MB ( 31 MiB) max; 26MB ( 25 MiB) avg; 33MB ( 31 MiB) peak Used in PS Old Gen pool: 166MB ( 158 MiB) max; 50MB ( 47 MiB) avg; 166MB ( 158 MiB) peak Allocated heap memory: 1324MB ( 1263 MiB) max; 855MB ( 816 MiB) avg Allocated non-heap memory: 33MB ( 31 MiB) max; 28MB ( 27 MiB) avg Total process virtual memory: 4969MB ( 4739 MiB) max; 4955MB ( 4725 MiB) avg Verification result: UNKNOWN, incomplete analysis. More details about the verification run can be found in the directory "./output".