./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_no-overflow/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_no-overflow/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.yml/witness.yml --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.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.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] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Setting "ana.int.interval" to true
[Info] function simple_fill_buf uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     simple_io
[Info]     verify_not_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     verify_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     test_unaligned_bulk
[Info]     usbtest_ioctl
[Info]     main
[Info]     usbtest_ioctl
[Info]     main
[Info]     unlink1
[Info]     unlink_simple
[Info]     usbtest_ioctl
[Info]     main
[Info]     unlink_queued
[Info]     usbtest_ioctl
[Info]     main
[Info] function simple_check_buf uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     check_guard_bytes
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     buffer_offset
[Info]   "up":
[Info]     simple_io
[Info]     verify_not_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     verify_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     test_unaligned_bulk
[Info]     usbtest_ioctl
[Info]     main
[Info]     usbtest_ioctl
[Info]     main
[Info]     unlink1
[Info]     unlink_simple
[Info]     usbtest_ioctl
[Info]     main
[Info] function simple_io uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     wait_for_completion_timeout
[Info]     __VERIFIER_nondet_ulong
[Info]     msecs_to_jiffies
[Info]     __VERIFIER_nondet_ulong
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     ldv_usb_submit_urb_21
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_submit_urb
[Info]     __VERIFIER_nondet_int
[Info]     usb_kill_urb
[Info]     init_completion
[Info]     __init_waitqueue_head
[Info]     simple_fill_buf
[Info]     simple_check_buf
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     check_guard_bytes
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     buffer_offset
[Info]   "up":
[Info]     verify_not_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     usbtest_ioctl
[Info]     verify_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     usbtest_ioctl
[Info]     test_unaligned_bulk
[Info]     usbtest_ioctl
[Info]     main
[Info]     usbtest_ioctl
[Info]     main
[Info] function alloc_sglist uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     sg_init_table
[Info]     kmalloc_array
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     kzalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     sg_set_buf
[Info]     ldv__builtin_expect
[Info]     __phys_addr
[Info]     __VERIFIER_nondet_ulong
[Info]     __virt_addr_valid
[Info]     __VERIFIER_nondet_bool
[Info]     sg_set_page
[Info]     sg_assign_page
[Info]     ldv__builtin_expect
[Info]     free_sglist
[Info]     kfree
[Info]     sg_page
[Info]     ldv__builtin_expect
[Info]     sg_virt
[Info]     lowmem_page_address
[Info]     sg_page
[Info]     ldv__builtin_expect
[Info]   "up":
[Info]     usbtest_ioctl
[Info]     main
[Info] function ctrl_complete uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     complete
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     ldv_usb_submit_urb_22
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_submit_urb
[Info]     __VERIFIER_nondet_int
[Info]     usb_unlink_urb
[Info]     __VERIFIER_nondet_int
[Info]     spin_lock
[Info]     ldv_spin_lock
[Info]     ldv_spin_lock_1
[Info]     _raw_spin_lock
[Info]     spin_unlock
[Info]     ldv_spin_unlock
[Info]     ldv_spin_unlock_5
[Info]     _raw_spin_unlock
[Info]   "up":
[Info] function test_ctrl_queue uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __raw_spin_lock_init
[Info]     wait_for_completion
[Info]     kfree
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     ldv_usb_submit_urb_23
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_submit_urb
[Info]     __VERIFIER_nondet_int
[Info]     spinlock_check
[Info]     spin_lock_irq
[Info]     ldv_spin_lock
[Info]     ldv_spin_lock_irq_4
[Info]     _raw_spin_lock_irq
[Info]     spin_unlock_irq
[Info]     ldv_spin_unlock
[Info]     ldv_spin_unlock_irq_7
[Info]     _raw_spin_unlock_irq
[Info]     init_completion
[Info]     __init_waitqueue_head
[Info]     kmalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     ldv_kmalloc_12
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     kcalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     ldv_kcalloc_14
[Info]     kmalloc_array
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     __create_pipe
[Info]     testdev_to_usbdev
[Info]     interface_to_usbdev
[Info]     simple_alloc_urb
[Info]     usbtest_alloc_urb
[Info]     ldv_usb_alloc_urb_19
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_alloc_urb
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     usb_free_urb
[Info]     ldv_usb_alloc_coherent_20
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_alloc_coherent
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     kmalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     ldv_kmalloc_12
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     usb_fill_bulk_urb
[Info]     simple_free_urb
[Info]     kfree
[Info]     usb_free_urb
[Info]     usb_free_coherent
[Info]     buffer_offset
[Info]   "up":
[Info]     usbtest_ioctl
[Info]     main
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Error][Analyzer] About to crash!

Fatal error: exception Failure("Yaml_unix.of_file: /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_no-overflow/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.yml/witness.yml: No such file or directory")
