- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35a08d14-11a8-43c4-9861-c27e984e788d
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 5972
    column: 3
    function: ldv_dispatch_default_register_7_5_4
  location_invariant:
    string: '! multithreaded || (pmutex_s_mutex_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4533529-d3ad-43e0-9736-07b9d6c43abd
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6010
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || (pmutex_s_mutex_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69e655e8-8bbf-42a4-b040-7d59e01f188b
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6042
    column: 3
    function: ldv_dispatch_irq_register_7_3
  location_invariant:
    string: '! multithreaded || (pmutex_s_mutex_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c45d8d0-80d4-4ef1-8780-f204042e6dfe
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6059
    column: 3
    function: ldv_dispatch_register_9_3
  location_invariant:
    string: '! multithreaded || (pmutex_s_mutex_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b9349d0-d754-47db-93ce-ff2a53d228d3
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 5972
    column: 3
    function: ldv_dispatch_default_register_7_5_4
  location_invariant:
    string: '! multithreaded || (smutex_dev_lock_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb5de0d9-a451-4c46-bf80-66e8fbbfd3d7
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6010
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || (smutex_dev_lock_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 442d4b47-b63e-432a-b216-8dcc7c0856c0
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6042
    column: 3
    function: ldv_dispatch_irq_register_7_3
  location_invariant:
    string: '! multithreaded || (smutex_dev_lock_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b77cfe62-80af-4bee-8a49-6aa6ccde836c
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6059
    column: 3
    function: ldv_dispatch_register_9_3
  location_invariant:
    string: '! multithreaded || (smutex_dev_lock_of_mcam_camera_locked || ((((((((((((((((unsigned
      int )__mod_pci_device_table.class == 0U && (unsigned int )__mod_pci_device_table.class_mask
      == 0U) && (unsigned int )__mod_pci_device_table.device == 0U) && (unsigned int
      )__mod_pci_device_table.subdevice == 0U) && (unsigned int )__mod_pci_device_table.subvendor
      == 0U) && (unsigned int )__mod_pci_device_table.vendor == 0U) && (unsigned long
      )__mod_pci_device_table.driver_data == 0UL) && (__this_module.sig_ok == (_Bool)0
      || __this_module.sig_ok == (_Bool)1)) && (x86_dma_fallback_dev.offline == (_Bool)0
      || x86_dma_fallback_dev.offline == (_Bool)1)) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45284d8f-97c9-415b-bcba-6c0a4bf19a43
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 5972
    column: 3
    function: ldv_dispatch_default_register_7_5_4
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff15dad4-1fa3-4a2a-81d6-ea63b42baa2b
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6010
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af0ee627-3b50-4387-83cc-188a749a407c
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6042
    column: 3
    function: ldv_dispatch_irq_register_7_3
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f7334d0-6e88-4ca1-9506-14ba18b55689
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6059
    column: 3
    function: ldv_dispatch_register_9_3
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a82b4e74-00f9-4432-aaed-45d3ec51f939
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 5972
    column: 3
    function: ldv_dispatch_default_register_7_5_4
  location_invariant:
    string: '! multithreaded || (((((((unsigned int )__mod_pci_device_table.class
      == 0U && (unsigned int )__mod_pci_device_table.class_mask == 0U) && (unsigned
      int )__mod_pci_device_table.device == 0U) && (unsigned int )__mod_pci_device_table.subdevice
      == 0U) && (unsigned int )__mod_pci_device_table.subvendor == 0U) && (unsigned
      int )__mod_pci_device_table.vendor == 0U) && (unsigned long )__mod_pci_device_table.driver_data
      == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7a69bb0-08be-421e-9cc1-2c352a8abd57
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6010
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || (((((((unsigned int )__mod_pci_device_table.class
      == 0U && (unsigned int )__mod_pci_device_table.class_mask == 0U) && (unsigned
      int )__mod_pci_device_table.device == 0U) && (unsigned int )__mod_pci_device_table.subdevice
      == 0U) && (unsigned int )__mod_pci_device_table.subvendor == 0U) && (unsigned
      int )__mod_pci_device_table.vendor == 0U) && (unsigned long )__mod_pci_device_table.driver_data
      == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13b2f51c-a921-4381-a918-bc63be9a6b49
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6042
    column: 3
    function: ldv_dispatch_irq_register_7_3
  location_invariant:
    string: '! multithreaded || (((((((unsigned int )__mod_pci_device_table.class
      == 0U && (unsigned int )__mod_pci_device_table.class_mask == 0U) && (unsigned
      int )__mod_pci_device_table.device == 0U) && (unsigned int )__mod_pci_device_table.subdevice
      == 0U) && (unsigned int )__mod_pci_device_table.subvendor == 0U) && (unsigned
      int )__mod_pci_device_table.vendor == 0U) && (unsigned long )__mod_pci_device_table.driver_data
      == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5d677da-ed2e-41a6-8eee-a26229bd8487
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6059
    column: 3
    function: ldv_dispatch_register_9_3
  location_invariant:
    string: '! multithreaded || (((((((unsigned int )__mod_pci_device_table.class
      == 0U && (unsigned int )__mod_pci_device_table.class_mask == 0U) && (unsigned
      int )__mod_pci_device_table.device == 0U) && (unsigned int )__mod_pci_device_table.subdevice
      == 0U) && (unsigned int )__mod_pci_device_table.subvendor == 0U) && (unsigned
      int )__mod_pci_device_table.vendor == 0U) && (unsigned long )__mod_pci_device_table.driver_data
      == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79896276-b337-4980-a2bb-b678c8d85e4c
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 5972
    column: 3
    function: ldv_dispatch_default_register_7_5_4
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84a95bad-2973-4a03-9f85-1577831cffd8
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6010
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e06051f-acfd-4c5f-bf4a-63f0b9245859
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6042
    column: 3
    function: ldv_dispatch_irq_register_7_3
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58624666-3e65-49f5-bfc2-2a350c1ed36d
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6059
    column: 3
    function: ldv_dispatch_register_9_3
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: a06d24dc-d198-4f46-857f-0cf8cce722ea
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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: 1458dedb-11c8-4c60-94ba-4743633daaa5
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 6008
    column: 3
    function: ldv_dispatch_insmod_register_10_3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: d8fa063f-f8ea-4f21-9eba-4b30d46bbe51
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_s_mutex_of_mcam_camera_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e7801f2-a954-47d4-9416-b9dd716762bd
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_s_mutex_of_mcam_camera_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 11201
    column: 3
    function: ldv_mutex_lock_s_mutex_of_mcam_camera
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: cb7f96bf-0ec3-432f-b96d-2a9574eda511
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_dev_lock_of_mcam_camera_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 590b6575-0b68-4cfb-a356-215e81c59755
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_dev_lock_of_mcam_camera_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 11399
    column: 3
    function: ldv_spin_unlock_dev_lock_of_mcam_camera
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 82737f86-0b16-4a6c-afcd-7ec3822083af
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_dev_lock_of_mcam_camera_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 11390
    column: 3
    function: ldv_spin_lock_dev_lock_of_mcam_camera
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cc57e41f-24ff-4b32-86f4-b7d1d0dd34cb
    creation_time: 2024-04-26T10:45:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-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--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
        : c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_s_mutex_of_mcam_camera_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 11265
    column: 3
    function: ldv_mutex_unlock_s_mutex_of_mcam_camera
