Fixing: byte_update of unknown width: byte_update_little_endian

[marek-trtik]

benchmark: ldv-memsafety/memleaks_test12_false-valid-free.i

./cbmc --graphml-witness witness.graphml --32 --propertyfile ../../sv-benchmarks/c/MemSafety.prp ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i

--------------------------------------------------------------------------------

Unwind: 2
CBMC version 5.8 64-bit x86_64 linux
Parsing ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i
Converting
Type-checking memleaks_test12_false-valid-free
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
file ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i line 1282 function ldv_kref_sub: replacing function pointer by 1 possible targets
file ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i line 1508 function ldv_i2c_transfer: replacing function pointer by 1 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
Unwinding loop master_xfer.0 iteration 1 (2 max) file ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i line 1487 function master_xfer thread 0
Not unwinding loop master_xfer.0 iteration 2 (2 max) file ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i line 1487 function master_xfer thread 0
Unwinding loop ldv_destroy_msgs.0 iteration 1 (2 max) file ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i line 1179 function ldv_destroy_msgs thread 0
Not unwinding loop ldv_destroy_msgs.0 iteration 2 (2 max) file ../../sv-benchmarks/c/ldv-memsafety/memleaks_test12_false-valid-free.i line 1179 function ldv_destroy_msgs thread 0
size of program expression: 2509 steps
simple slicing removed 1 assignments
Generated 438 VCC(s), 388 remaining after simplification
Passing problem to propositional reduction
converting SSA
byte_update of unknown width:
byte_update_little_endian
  * type: array
      * size: symbol
          * type: unsignedbv
              * width: 32
              * #source_location: 
                * file: <built-in-additions>
                * line: 1
                * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
              * #typedef: __CPROVER_size_t
              * #c_type: unsigned_int
          * identifier: symex_dynamic::dynamic_object_size8#1
          * expression: symbol
              * type: unsignedbv
                  * width: 32
                  * #source_location: 
                    * file: <built-in-additions>
                    * line: 1
                    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                  * #typedef: __CPROVER_size_t
                  * #c_type: unsigned_int
              * identifier: symex_dynamic::dynamic_object_size8
          * L2: 1
          * L1_object_identifier: symex_dynamic::dynamic_object_size8
          * #SSA_symbol: 1
      * #dynamic: 1
      0: unsignedbv
          * width: 8
          * #c_type: unsigned_char
  0: if
      * type: array
          * size: symbol
              * type: unsignedbv
                  * width: 32
                  * #source_location: 
                    * file: <built-in-additions>
                    * line: 1
                    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                  * #typedef: __CPROVER_size_t
                  * #c_type: unsigned_int
              * identifier: symex_dynamic::dynamic_object_size8#1
              * expression: symbol
                  * type: unsignedbv
                      * width: 32
                      * #source_location: 
                        * file: <built-in-additions>
                        * line: 1
                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                      * #typedef: __CPROVER_size_t
                      * #c_type: unsigned_int
                  * identifier: symex_dynamic::dynamic_object_size8
              * L2: 1
              * L1_object_identifier: symex_dynamic::dynamic_object_size8
              * #SSA_symbol: 1
          * #dynamic: 1
          0: unsignedbv
              * width: 8
              * #c_type: unsigned_char
      0: =
          * type: bool
          0: typecast
              * type: pointer
                  * width: 32
                  0: unsignedbv
                      * width: 8
                      * #c_type: unsigned_char
              0: symbol
                  * type: pointer
                      * width: 32
                      * #source_location: 
                        * file: <built-in-additions>
                        * line: 42
                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                      0: empty
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 42
                            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                          * #constant: 1
                  * identifier: memcpy::dst!0@2#1
                  * expression: symbol
                      * type: pointer
                          * width: 32
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 42
                            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                          0: empty
                              * #source_location: 
                                * file: <built-in-additions>
                                * line: 42
                                * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                              * #constant: 1
                      * identifier: memcpy::dst
                  * L0: 0
                  * L1: 2
                  * L2: 1
                  * L1_object_identifier: memcpy::dst!0@2
                  * #SSA_symbol: 1
          1: address_of
              * type: pointer
                  * width: 32
                  0: unsignedbv
                      * width: 8
                      * #c_type: unsigned_char
              0: index
                  * type: unsignedbv
                      * width: 8
                      * #c_type: unsigned_char
                  0: symbol
                      * type: array
                          * size: symbol
                              * type: unsignedbv
                                  * width: 32
                                  * #source_location: 
                                    * file: <built-in-additions>
                                    * line: 1
                                    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                                  * #typedef: __CPROVER_size_t
                                  * #c_type: unsigned_int
                              * identifier: symex_dynamic::dynamic_object_size8#1
                              * expression: symbol
                                  * type: unsignedbv
                                      * width: 32
                                      * #source_location: 
                                        * file: <built-in-additions>
                                        * line: 1
                                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                                      * #typedef: __CPROVER_size_t
                                      * #c_type: unsigned_int
                                  * identifier: symex_dynamic::dynamic_object_size8
                              * L2: 1
                              * L1_object_identifier: symex_dynamic::dynamic_object_size8
                              * #SSA_symbol: 1
                          * #dynamic: 1
                          0: unsignedbv
                              * width: 8
                              * #c_type: unsigned_char
                      * identifier: symex_dynamic::dynamic_object8
                      * expression: symbol
                          * type: array
                              * size: symbol
                                  * type: unsignedbv
                                      * width: 32
                                      * #source_location: 
                                        * file: <built-in-additions>
                                        * line: 1
                                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                                      * #typedef: __CPROVER_size_t
                                      * #c_type: unsigned_int
                                  * identifier: symex_dynamic::dynamic_object_size8#1
                                  * expression: symbol
                                      * type: unsignedbv
                                          * width: 32
                                          * #source_location: 
                                            * file: <built-in-additions>
                                            * line: 1
                                            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                                          * #typedef: __CPROVER_size_t
                                          * #c_type: unsigned_int
                                      * identifier: symex_dynamic::dynamic_object_size8
                                  * L2: 1
                                  * L1_object_identifier: symex_dynamic::dynamic_object_size8
                                  * #SSA_symbol: 1
                              * #dynamic: 1
                              0: unsignedbv
                                  * width: 8
                                  * #c_type: unsigned_char
                          * identifier: symex_dynamic::dynamic_object8
                      * L1_object_identifier: symex_dynamic::dynamic_object8
                      * #SSA_symbol: 1
                  1: constant
                      * type: signedbv
                          * width: 32
                          * #c_type: signed_int
                      * value: 00000000000000000000000000000000
                      * #source_location: 
                        * file: <built-in-additions>
                        * line: 68
                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                      * #base: 10
      1: symbol
          * type: array
              * size: symbol
                  * type: unsignedbv
                      * width: 32
                      * #source_location: 
                        * file: <built-in-additions>
                        * line: 1
                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                      * #typedef: __CPROVER_size_t
                      * #c_type: unsigned_int
                  * identifier: symex_dynamic::dynamic_object_size8#1
                  * expression: symbol
                      * type: unsignedbv
                          * width: 32
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 1
                            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                          * #typedef: __CPROVER_size_t
                          * #c_type: unsigned_int
                      * identifier: symex_dynamic::dynamic_object_size8
                  * L2: 1
                  * L1_object_identifier: symex_dynamic::dynamic_object_size8
                  * #SSA_symbol: 1
              * #dynamic: 1
              0: unsignedbv
                  * width: 8
                  * #c_type: unsigned_char
          * identifier: symex_dynamic::dynamic_object8#0
          * expression: symbol
              * type: array
                  * size: symbol
                      * type: unsignedbv
                          * width: 32
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 1
                            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                          * #typedef: __CPROVER_size_t
                          * #c_type: unsigned_int
                      * identifier: symex_dynamic::dynamic_object_size8#1
                      * expression: symbol
                          * type: unsignedbv
                              * width: 32
                              * #source_location: 
                                * file: <built-in-additions>
                                * line: 1
                                * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                              * #typedef: __CPROVER_size_t
                              * #c_type: unsigned_int
                          * identifier: symex_dynamic::dynamic_object_size8
                      * L2: 1
                      * L1_object_identifier: symex_dynamic::dynamic_object_size8
                      * #SSA_symbol: 1
                  * #dynamic: 1
                  0: unsignedbv
                      * width: 8
                      * #c_type: unsigned_char
              * identifier: symex_dynamic::dynamic_object8
          * L2: 0
          * L1_object_identifier: symex_dynamic::dynamic_object8
          * #SSA_symbol: 1
      2: array
          * type: array
              * size: symbol
                  * type: unsignedbv
                      * width: 32
                      * #source_location: 
                        * file: <built-in-additions>
                        * line: 1
                        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                      * #typedef: __CPROVER_size_t
                      * #c_type: unsigned_int
                  * identifier: symex_dynamic::dynamic_object_size8#1
                  * expression: symbol
                      * type: unsignedbv
                          * width: 32
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 1
                            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
                          * #typedef: __CPROVER_size_t
                          * #c_type: unsigned_int
                      * identifier: symex_dynamic::dynamic_object_size8
                  * L2: 1
                  * L1_object_identifier: symex_dynamic::dynamic_object_size8
                  * #SSA_symbol: 1
              * #dynamic: 1
              0: unsignedbv
                  * width: 8
                  * #c_type: unsigned_char
  1: constant
      * type: signedbv
          * width: 32
          * #c_type: signed_int
      * value: 00000000000000000000000000000000
      * #source_location: 
        * file: <built-in-additions>
        * line: 68
        * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
      * #base: 10
  2: symbol
      * type: array
          * size: symbol
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * identifier: memcpy::1::src_n$array_size0!0@2#2
              * expression: symbol
                  * type: signedbv
                      * width: 32
                      * #c_type: signed_int
                  * identifier: memcpy::1::src_n$array_size0
              * L0: 0
              * L1: 2
              * L2: 2
              * L1_object_identifier: memcpy::1::src_n$array_size0!0@2
              * #SSA_symbol: 1
          * #source_location: 
            * file: <builtin-library-memcpy>
            * line: 34
            * function: memcpy
            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
          0: signedbv
              * width: 8
              * #c_type: char
      * identifier: memcpy::1::src_n!0@2#2
      * expression: symbol
          * type: array
              * size: symbol
                  * type: signedbv
                      * width: 32
                      * #c_type: signed_int
                  * identifier: memcpy::1::src_n$array_size0!0@2#2
                  * expression: symbol
                      * type: signedbv
                          * width: 32
                          * #c_type: signed_int
                      * identifier: memcpy::1::src_n$array_size0
                  * L0: 0
                  * L1: 2
                  * L2: 2
                  * L1_object_identifier: memcpy::1::src_n$array_size0!0@2
                  * #SSA_symbol: 1
              * #source_location: 
                * file: <builtin-library-memcpy>
                * line: 34
                * function: memcpy
                * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
              0: signedbv
                  * width: 8
                  * #c_type: char
          * identifier: memcpy::1::src_n
          * #source_location: 
            * file: <builtin-library-memcpy>
            * line: 34
            * function: memcpy
            * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_c4ffb3eb-9a4a-4dad-af76-b74c4fcf5024/bin-2018/cbmc
      * L0: 0
      * L1: 2
      * L2: 2
      * L1_object_identifier: memcpy::1::src_n!0@2
      * #SSA_symbol: 1
EC=6
UNKNOWN

[marek-trtik]

Here is the complete list of benchmarks with this issue:

{
    "falsification": [
        "busybox-1.22.0/chgrp-incomplete_false-no-overflow.i",
        "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i",
        "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i",
        "busybox-1.22.0/chroot-incomplete_false-no-overflow.i",
        "busybox-1.22.0/cut_false-no-overflow.i",
        "busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/date_false-no-overflow.i",
        "busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/fold_false-no-overflow.i",
        "busybox-1.22.0/head_false-no-overflow.i",
        "busybox-1.22.0/head_false-valid-deref.i",
        "busybox-1.22.0/logname_false-no-overflow.i",
        "busybox-1.22.0/mkfifo-incomplete_false-no-overflow.i",
        "busybox-1.22.0/printf_false-no-overflow.i",
        "busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/readlink_false-no-overflow.i",
        "busybox-1.22.0/realpath_false-no-overflow.i",
        "busybox-1.22.0/sleep_false-no-overflow.i",
        "busybox-1.22.0/sleep_false-valid-deref.i",
        "busybox-1.22.0/stty_false-no-overflow.i",
        "busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i",
        "busybox-1.22.0/sync_false-no-overflow.i",
        "busybox-1.22.0/tac_false-no-overflow.i",
        "busybox-1.22.0/tee_false-no-overflow.i",
        "busybox-1.22.0/uname_false-no-overflow.i",
        "busybox-1.22.0/uniq_false-no-overflow.i",
        "busybox-1.22.0/usleep_false-no-overflow.i",
        "busybox-1.22.0/who_false-no-overflow.i",
        "busybox-1.22.0/yes_false-no-overflow.i",
        "ldv-memsafety/memleaks_test12_false-valid-free.i"
    ],
    "issues": [
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.usleep_false-no-overflow.i.log": "busybox-1.22.0/usleep_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.head_false-no-overflow.i.log": "busybox-1.22.0/head_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.tee_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.printf_false-no-overflow.i.log": "busybox-1.22.0/printf_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.fold_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.uname_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.chroot-incomplete_false-no-overflow.i.log": "busybox-1.22.0/chroot-incomplete_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.readlink_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.mkfifo-incomplete_false-no-overflow.i.log": "busybox-1.22.0/mkfifo-incomplete_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.date_false-no-overflow.i.log": "busybox-1.22.0/date_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.uniq_false-no-overflow.i.log": "busybox-1.22.0/uniq_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.sleep_false-no-overflow.i.log": "busybox-1.22.0/sleep_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.date_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.head_true-no-overflow_true-valid-deref.i.log": "busybox-1.22.0/head_true-no-overflow_true-valid-deref.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.chroot-incomplete_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.realpath_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.sync_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.yes_false-no-overflow.i.log": "busybox-1.22.0/yes_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.readlink_false-no-overflow.i.log": "busybox-1.22.0/readlink_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.who_false-no-overflow.i.log": "busybox-1.22.0/who_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.fold_false-no-overflow.i.log": "busybox-1.22.0/fold_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.cut_false-no-overflow.i.log": "busybox-1.22.0/cut_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.sync_false-no-overflow.i.log": "busybox-1.22.0/sync_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.tac_false-no-overflow.i.log": "busybox-1.22.0/tac_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.sleep_true-no-overflow_true-valid-deref.i.log": "busybox-1.22.0/sleep_true-no-overflow_true-valid-deref.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.uniq_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.tee_false-no-overflow.i.log": "busybox-1.22.0/tee_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.realpath_false-no-overflow.i.log": "busybox-1.22.0/realpath_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.logname_false-no-overflow.i.log": "busybox-1.22.0/logname_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.yes_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.usleep_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.logname_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.chgrp-incomplete_true-no-overflow_false-valid-memtrack.i.log": "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.stty_false-no-overflow.i.log": "busybox-1.22.0/stty_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.chgrp-incomplete_false-no-overflow.i.log": "busybox-1.22.0/chgrp-incomplete_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.tac_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.who_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1542.logfiles/sv-comp18.uname_false-no-overflow.i.log": "busybox-1.22.0/uname_false-no-overflow.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.tee_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.fold_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.uname_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.readlink_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.head_false-valid-deref.i.log": "busybox-1.22.0/head_false-valid-deref.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.date_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.chroot-incomplete_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.realpath_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.sync_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.sleep_false-valid-deref.i.log": "busybox-1.22.0/sleep_false-valid-deref.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.memleaks_test12_false-valid-free.i.log": "ldv-memsafety/memleaks_test12_false-valid-free.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.uniq_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.memleaks_test12_true-valid-memsafety.i.log": "ldv-memsafety/memleaks_test12_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.yes_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.usleep_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.logname_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.chgrp-incomplete_true-no-overflow_false-valid-memtrack.i.log": "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.tac_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i"
        },
        {
            "/home/marek/root/SV-COMP-2018/RESULTSDB/2017_11_24 (sosy)/cbmc.2017-11-24_1408.logfiles/sv-comp18.who_true-no-overflow_true-valid-memsafety.i.log": "busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i"
        }
    ]
}

[marek-trtik]

These benchmarks are complicated and we are running out of time.