- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c3536e1-67a5-4ddc-9871-81b99b16399f
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || jiffies == 0UL'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38d19f82-2f61-41e6-9b6d-fba5d89b2858
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || jiffies == 0UL'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bf264a6-4ebc-4df8-bb20-3010480665af
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((nvram_fops.check_flags ==
      0 && nvram_fops.compat_ioctl == 0) && nvram_fops.dir_notify == 0) && nvram_fops.fasync
      == 0) && nvram_fops.flock == 0) && nvram_fops.flush == 0) && nvram_fops.fsync
      == 0) && nvram_fops.get_unmapped_area == 0) && nvram_fops.ioctl == 0) && nvram_fops.llseek
      == & nvram_llseek) && nvram_fops.lock == 0) && nvram_fops.mmap == 0) && nvram_fops.open
      == 0) && nvram_fops.open_exec == 0) && nvram_fops.owner == 0) && nvram_fops.poll
      == 0) && nvram_fops.read == & read_nvram) && nvram_fops.readdir == 0) && nvram_fops.readv
      == 0) && nvram_fops.release == 0) && nvram_fops.sendfile == 0) && nvram_fops.sendpage
      == 0) && nvram_fops.unlocked_ioctl == & nvram_unlocked_ioctl) && nvram_fops.write
      == & write_nvram) && nvram_fops.writev == 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 586feeac-471e-4e0b-84ab-cd1de2e1e2f2
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((nvram_fops.check_flags ==
      0 && nvram_fops.compat_ioctl == 0) && nvram_fops.dir_notify == 0) && nvram_fops.fasync
      == 0) && nvram_fops.flock == 0) && nvram_fops.flush == 0) && nvram_fops.fsync
      == 0) && nvram_fops.get_unmapped_area == 0) && nvram_fops.ioctl == 0) && nvram_fops.llseek
      == & nvram_llseek) && nvram_fops.lock == 0) && nvram_fops.mmap == 0) && nvram_fops.open
      == 0) && nvram_fops.open_exec == 0) && nvram_fops.owner == 0) && nvram_fops.poll
      == 0) && nvram_fops.read == & read_nvram) && nvram_fops.readdir == 0) && nvram_fops.readv
      == 0) && nvram_fops.release == 0) && nvram_fops.sendfile == 0) && nvram_fops.sendpage
      == 0) && nvram_fops.unlocked_ioctl == & nvram_unlocked_ioctl) && nvram_fops.write
      == & write_nvram) && nvram_fops.writev == 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57737aaa-c828-4dc2-8668-5f25494e42d4
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || (unsigned int )default_alloc_size == 4U'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d2a4dd7-ec13-47e1-a4b8-921e27929fed
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || (unsigned int )default_alloc_size == 4U'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58690f44-e328-4adf-b966-7ccb9eb2d00d
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_exit == & nvram_cleanup'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bae80ef7-7a3e-4aab-999d-96807127d9ff
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_exit == & nvram_cleanup'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fa92b78-f600-45f2-89bd-d3b20a804d97
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_init == & nvram_init'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95e28c84-f92d-47a8-9443-0592d822101f
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_init == & nvram_init'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 37d0ef97-23ad-4350-9c68-9866dc1911b2
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94095754-92f2-48a7-8f5e-958554a946c6
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 462
    column: 3
    function: mutex_unlock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2400c072-37cb-49dc-a59b-6eb6e59cf320
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 460
    column: 3
    function: mutex_unlock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 910a3139-abb5-4e45-ad62-8dc88c53dbac
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 442
    column: 3
    function: mutex_lock
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 68499003-bd03-4a8a-98dc-3f698f2af2c9
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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: 631bafdd-ec7f-4d17-b2f9-6e84fd475b62
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6861
    column: 2
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9da0e296-f6c0-4168-83f5-9e80a6ee0d7d
    creation_time: 2024-04-30T09:38:40Z
    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/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 445
    column: 3
    function: mutex_lock
