- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0294cdc4-208a-4efc-93e2-0a4bfe9a08ae
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (smutex_buflock_of_adu_device_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8feb7d8a-3f0b-4987-a0e7-978a9238c9bb
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (smutex_buflock_of_adu_device_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3216118d-a81f-48d2-a53f-2a40b1309fdf
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (smutex_buflock_of_adu_device_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e565e099-0000-4c91-8622-5c34fa9a9927
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (((((((((((((unsigned char )__mod_usb_device_table.bDeviceClass
      == (unsigned char)0 && (unsigned char )__mod_usb_device_table.bDeviceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bDeviceSubClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceNumber
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceSubClass
      == (unsigned char)0) && (unsigned short )__mod_usb_device_table.bcdDevice_hi
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.bcdDevice_lo
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.idProduct ==
      (unsigned short)0) && (unsigned short )__mod_usb_device_table.idVendor == (unsigned
      short)0) && (unsigned short )__mod_usb_device_table.match_flags == (unsigned
      short)0) && (unsigned long )__mod_usb_device_table.driver_info == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b09032a-0f8c-454b-9f24-c7bf22499ac5
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (((((((((((((unsigned char )__mod_usb_device_table.bDeviceClass
      == (unsigned char)0 && (unsigned char )__mod_usb_device_table.bDeviceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bDeviceSubClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceNumber
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceSubClass
      == (unsigned char)0) && (unsigned short )__mod_usb_device_table.bcdDevice_hi
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.bcdDevice_lo
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.idProduct ==
      (unsigned short)0) && (unsigned short )__mod_usb_device_table.idVendor == (unsigned
      short)0) && (unsigned short )__mod_usb_device_table.match_flags == (unsigned
      short)0) && (unsigned long )__mod_usb_device_table.driver_info == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbfaf660-69df-4977-adaa-075aba414021
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (((((((((((((unsigned char )__mod_usb_device_table.bDeviceClass
      == (unsigned char)0 && (unsigned char )__mod_usb_device_table.bDeviceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bDeviceSubClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceNumber
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceSubClass
      == (unsigned char)0) && (unsigned short )__mod_usb_device_table.bcdDevice_hi
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.bcdDevice_lo
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.idProduct ==
      (unsigned short)0) && (unsigned short )__mod_usb_device_table.idVendor == (unsigned
      short)0) && (unsigned short )__mod_usb_device_table.match_flags == (unsigned
      short)0) && (unsigned long )__mod_usb_device_table.driver_info == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb201fae-22c3-40fe-8fb3-974825902862
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (pmutex_mtx_of_adu_device_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4be49ebc-c143-4b01-bc32-fdb503d9a26f
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (pmutex_mtx_of_adu_device_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b7b962-4f39-4c92-a6c5-67140b808f5b
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (pmutex_mtx_of_adu_device_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb725723-e86c-4c35-a8c2-18d75c9b68da
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (pmutex_adutux_mutex_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 515231fa-5f4e-485b-b8de-a2198984507d
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (pmutex_adutux_mutex_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad59039e-1b81-4555-9c4c-ead6a8a27468
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (pmutex_adutux_mutex_locked || (((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c20c8d89-602a-4b45-a10a-5b8146d013e1
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c7839e4-8cbe-4a7c-9001-6e58e32d4ae3
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7123
    column: 5
    function: ldv_mutex_lock_interruptible_or_killable_mtx_of_adu_device
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9f6488f3-81e3-4567-bc0c-34dde4616d22
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7109
    column: 3
    function: ldv_mutex_lock_mtx_of_adu_device
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 28d5bbb5-bb10-4f5b-850a-56a998e468aa
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_buflock_of_adu_device_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3a9e695b-7cc6-4c97-95cf-18a9717a090b
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_buflock_of_adu_device_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7372
    column: 3
    function: ldv_spin_lock_buflock_of_adu_device
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e898d1c8-c772-4f65-b152-26890ceef23e
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_buflock_of_adu_device_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7381
    column: 3
    function: ldv_spin_unlock_buflock_of_adu_device
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 25568ec5-bd96-4c82-a37a-d2b8ce30399a
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e8846595-c4d6-493a-9e60-866795b83c62
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5994
    column: 3
    function: ldv_dispatch_insmod_register_7_3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 207cd4c4-f03c-4c10-9b08-fb38b3f81b01
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 46b720d6-fe93-4bb0-9e86-212816e9b652
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6951
    column: 3
    function: ldv_mutex_unlock_adutux_mutex
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c78b4364-518b-48bd-a239-083f1229203f
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6901
    column: 5
    function: ldv_mutex_lock_interruptible_or_killable_adutux_mutex
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6c6f8392-4076-48ee-9fce-2cf3f86ac73f
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7173
    column: 3
    function: ldv_mutex_unlock_mtx_of_adu_device
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f14dd2bf-85f1-4f92-9391-bb9394555acc
    creation_time: 2024-04-29T11:53:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6887
    column: 3
    function: ldv_mutex_lock_adutux_mutex
