- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff5507e4-0332-4ff8-b626-9c296def5c94
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 46fb65e9-4f05-4a17-9be0-73af2b2fc812
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 1a3ab9ad-cee8-45aa-9351-f8edc54ff035
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6d8ffb17-d021-4e2f-9ba3-17a816e6e24c
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: b6d847f0-3306-40c6-8e4c-671fce904d53
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 2b157a31-a108-40d5-845b-0d184abea7e1
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: e2fa81d1-0c89-41fa-bdf1-4bab5f67993a
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: b87ef53f-8c07-47cc-a330-dfcdd2b08daf
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: fdfa6047-d565-4b61-959f-b10084849319
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 36a9a015-f418-48d7-9cc3-331a5f2a4373
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: e572b31f-657f-4b4b-9b81-7c81873cd95c
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: ac1b8599-c96a-4474-955e-81dcb79b9895
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 01cac8b8-4e17-4461-b22f-1f8847c5c51f
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: cd2f0ce3-97f8-4a3b-bec7-a0607e7295fb
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 406e33b6-7f3c-4703-8857-cbf4e0e30bc2
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 5919b2de-c246-44cc-91bb-f0ce2ea80b87
    creation_time: 2024-04-29T11:02:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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
