./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-atm-eni.ko.cil.out.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] Setting "ana.int.interval" to true
[Info] function EVENT uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     rx_ident_err
[Info]     rx_aal0
[Info]     rx_aal5
[Info]     do_rx_dma
[Info]     discard
[Info]     rx_aal0
[Info]     rx_aal5
[Info]     rx_aal0
[Info]     rx_aal5
[Info]     discard
[Info]     rx_aal0
[Info]     rx_aal5
[Info]     rx_aal5
[Info]     rx_vcc
[Info]     poll_rx
[Info]     eni_tasklet
[Info]     poll_rx
[Info]     eni_tasklet
[Info]     get_service
[Info]     eni_tasklet
[Info]     dequeue_rx
[Info]     eni_tasklet
[Info]     close_rx
[Info]     eni_close
[Info]     main
[Info]     eni_open
[Info]     main
[Info]     put_dma
[Info]     do_tx
[Info]     poll_tx
[Info]     eni_tasklet
[Info]     eni_send
[Info]     main
[Info]     do_tx
[Info]     poll_tx
[Info]     eni_tasklet
[Info]     eni_send
[Info]     main
[Info]     bug_int
[Info]     eni_tasklet
[Info]     eni_int
[Info]     main
[Info]     eni_tasklet
[Info]     eni_open
[Info]     main
[Info] function event_dump uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     printk
[Info]     __VERIFIER_nondet_int
[Info]   "up":
[Info]     rx_ident_err
[Info]     rx_aal0
[Info]     rx_aal5
[Info]     bug_int
[Info]     eni_tasklet
[Info] function do_tx uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     printk
[Info]     __VERIFIER_nondet_int
[Info]     skb_queue_tail
[Info]     readl
[Info]     writel
[Info]     pci_map_single
[Info]     dma_map_single_attrs
[Info]     __phys_addr
[Info]     __VERIFIER_nondet_ulong
[Info]     debug_dma_map_page
[Info]     valid_dma_direction
[Info]     kmemcheck_mark_initialized
[Info]     get_dma_ops
[Info]     skb_end_pointer
[Info]     skb_headlen
[Info]     EVENT
[Info]     put_dma
[Info]     EVENT
[Info]   "up":
[Info]     poll_tx
[Info]     eni_tasklet
[Info]     eni_send
[Info]     main
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
