A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Found 55 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fe59110 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T10:41:18+01:00 | ||
4fe86eb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:23:07Z | ||
9c0b659 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T08:03:17+01:00 | ||
ee521a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T22:18:00+01:00 | ||
520ff52 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2023-12-18T01:35:40+01:00 | ||
ec695e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T12:35:07Z | ||
1886ebd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T13:18:14Z | ||
54d7ab5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T21:06:39Z | ||
b651ee6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T13:58:28Z | ||
08bdd98 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-19T01:13:36+01:00 | ||
01b69bc | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 13 | 2023-12-02T14:13:32Z | ||
6e5d4e6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | PredatorHP | 4 | 2023-11-30T08:24:56Z | ||
dce0358 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T15:27:25Z | ||
217ce36 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 738 | 2023-12-17T17:32:07+01:00 | ||
ce08af3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 13 | 2023-11-29T06:10:30Z | ||
330b486 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 8 | 2023-12-17T21:50:50+01:00 | 4efda52 | |
c0048af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:40:30+01:00 | ||
aaedb50 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:40:50Z | ||
3e3f079 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
cf20f4d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 13 | 2023-12-02T12:32:20Z | ||
9e23193 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T04:04:21Z | ||
b9228fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:49:37Z | ||
ab2bc58 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T21:19:03 | ||
02a6e56 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T14:03:22Z | ||
57955c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 7.4.0 kind | 3 | 2023-12-01T16:57:17Z | ||
5a061ea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-20T02:16:38+01:00 | ab2bc58 | |
10fa91f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-17T06:24:06+01:00 | 9e23193 | |
e1c083f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-05T14:20:44+01:00 | b1c3f30 | |
4dea057 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T16:29:28+01:00 | cbbe10c | |
9bcbe44 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T11:30:35+01:00 | cf20f4d | |
b07b019 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T18:35:36+01:00 | c0048af | |
52d3242 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T09:54:01+01:00 | aaedb50 | |
32667f0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T22:47:08+01:00 | 5d55f59 | |
35b66e0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T18:11:44+01:00 | 57955c4 | |
f01acad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T05:34:43+01:00 | ||
af4f7da | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T02:43:09+01:00 | b9228fe | |
8703ef2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T18:21:16+01:00 | 02a6e56 | |
3a407c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T07:56:06+01:00 | 3372908 | |
56d86da | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-04T00:04:46+01:00 | ||
a441f14 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-18T17:47:44+01:00 | ||
4efda52 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CBMC | 725 | 2023-12-17T15:46:59+01:00 | ||
b1c3f30 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Bubaak | 3 | 2023-12-05T10:31:07Z | ||
cbbe10c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:52:31Z | ||
5d55f59 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:50:58Z | ||
3372908 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 14 | 2023-11-29T03:00:39Z | ||
88b7de6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T14:18:57Z | ||
6c28908 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:43:40Z | ||
ba85deb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2023-12-19T22:03:43 | ||
514d11a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 725 | 2023-12-17T08:59:11+01:00 | ||
1d11e6f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T08:56:56Z | ||
cd10ff6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T09:45:16Z | ||
f12541e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T21:08:48Z | ||
ab3bd88 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: f927e826-4cd2-4f6a-97e5-ba55fc83f675 creation_time: '2023-11-29T04:00:39+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c : f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 32bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 25 column: 0 function: main value: ((i <= 2147483646) && (0 <= (i + 2147483648))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 28 column: 0 function: main value: ((i <= 2147483644) && (0 <= (i + 2147483648))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 0 function: foo value: (((((((i % 4294967296) <= 31) && (32 == size)) && (0 <= (i + 2147483648))) && (i == 0)) && (i <= 2147483645)) || ((((((i % 4294967296) <= 31) && (0 <= (i + 2147483648))) && (size <= 32)) && (1 <= i)) && (i <= 2147483645))) format: c_expression | correctness_witness | CPAchecker 2.3 | 10 | 2023-11-29T07:49:01+01:00 | ||
a7a7506 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 4ad5c713-554c-4e45-a69b-e98bd1fbdfa9 creation_time: '2023-12-02T13:32:20+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c : f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 32bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 25 column: 0 function: main value: ((0 <= i) && (i <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 28 column: 0 function: main value: ((0 <= i) && (i <= 2147483645)) format: c_expression | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T12:03:29+01:00 | ||
e673554 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: d2312ea7-1808-4581-9c5e-b259eadc6e5f creation_time: 2023-12-01T01:58:02Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''32bit'' ''../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c''' task: input_files: - ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c input_file_hashes: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df data_model: ILP32 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 8 function: foo value: 32 == size format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 8 function: foo value: size == 32 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 8 function: foo value: (((((((((((((((((((((((((((12 <= i && (-44LL + (long long )i) + (long long )size >= 0LL) && (20LL + (long long )i) - (long long )size >= 0LL) && (((i <= 31 && (-1LL - (long long )i) + (long long )size >= 0LL) && (63LL - (long long )i) - (long long )size >= 0LL) || ((i <= 32 && (0LL - (long long )i) + (long long )size >= 0LL) && (64LL - (long long )i) - (long long )size >= 0LL))) || (((((-43LL + (long long )i) + (long long )size >= 0LL && (-21LL - (long long )i) + (long long )size >= 0LL) && (21LL + (long long )i) - (long long )size >= 0LL) && (43LL - (long long )i) - (long long )size >= 0LL) && i == 11)) || (((((-43LL + (long long )i) + (long long )size >= 0LL && (-21LL - (long long )i) + (long long )size >= 0LL) && (21LL + (long long )i) - (long long )size >= 0LL) && (43LL - (long long )i) - (long long )size >= 0LL) && i == 11)) || (((((-42LL + (long long )i) + (long long )size >= 0LL && (-22LL - (long long )i) + (long long )size >= 0LL) && (22LL + (long long )i) - (long long )size >= 0LL) && (42LL - (long long )i) - (long long )size >= 0LL) && i == 10)) || (((((-42LL + (long long )i) + (long long )size >= 0LL && (-22LL - (long long )i) + (long long )size >= 0LL) && (22LL + (long long )i) - (long long )size >= 0LL) && (42LL - (long long )i) - (long long )size >= 0LL) && i == 10)) || (((((-41LL + (long long )i) + (long long )size >= 0LL && (-23LL - (long long )i) + (long long )size >= 0LL) && (23LL + (long long )i) - (long long )size >= 0LL) && (41LL - (long long )i) - (long long )size >= 0LL) && i == 9)) || (((((-41LL + (long long )i) + (long long )size >= 0LL && (-23LL - (long long )i) + (long long )size >= 0LL) && (23LL + (long long )i) - (long long )size >= 0LL) && (41LL - (long long )i) - (long long )size >= 0LL) && i == 9)) || (((((-40LL + (long long )i) + (long long )size >= 0LL && (-24LL - (long long )i) + (long long )size >= 0LL) && (24LL + (long long )i) - (long long )size >= 0LL) && (40LL - (long long )i) - (long long )size >= 0LL) && i == 8)) || (((((-40LL + (long long )i) + (long long )size >= 0LL && (-24LL - (long long )i) + (long long )size >= 0LL) && (24LL + (long long )i) - (long long )size >= 0LL) && (40LL - (long long )i) - (long long )size >= 0LL) && i == 8)) || (((((-39LL + (long long )i) + (long long )size >= 0LL && (-25LL - (long long )i) + (long long )size >= 0LL) && (25LL + (long long )i) - (long long )size >= 0LL) && (39LL - (long long )i) - (long long )size >= 0LL) && i == 7)) || (((((-39LL + (long long )i) + (long long )size >= 0LL && (-25LL - (long long )i) + (long long )size >= 0LL) && (25LL + (long long )i) - (long long )size >= 0LL) && (39LL - (long long )i) - (long long )size >= 0LL) && i == 7)) || (((((-38LL + (long long )i) + (long long )size >= 0LL && (-26LL - (long long )i) + (long long )size >= 0LL) && (26LL + (long long )i) - (long long )size >= 0LL) && (38LL - (long long )i) - (long long )size >= 0LL) && i == 6)) || (((((-38LL + (long long )i) + (long long )size >= 0LL && (-26LL - (long long )i) + (long long )size >= 0LL) && (26LL + (long long )i) - (long long )size >= 0LL) && (38LL - (long long )i) - (long long )size >= 0LL) && i == 6)) || (((((-37LL + (long long )i) + (long long )size >= 0LL && (-27LL - (long long )i) + (long long )size >= 0LL) && (27LL + (long long )i) - (long long )size >= 0LL) && (37LL - (long long )i) - (long long )size >= 0LL) && i == 5)) || (((((-37LL + (long long )i) + (long long )size >= 0LL && (-27LL - (long long )i) + (long long )size >= 0LL) && (27LL + (long long )i) - (long long )size >= 0LL) && (37LL - (long long )i) - (long long )size >= 0LL) && i == 5)) || (((((-36LL + (long long )i) + (long long )size >= 0LL && (-28LL - (long long )i) + (long long )size >= 0LL) && (28LL + (long long )i) - (long long )size >= 0LL) && (36LL - (long long )i) - (long long )size >= 0LL) && i == 4)) || (((((-36LL + (long long )i) + (long long )size >= 0LL && (-28LL - (long long )i) + (long long )size >= 0LL) && (28LL + (long long )i) - (long long )size >= 0LL) && (36LL - (long long )i) - (long long )size >= 0LL) && i == 4)) || (((((-35LL + (long long )i) + (long long )size >= 0LL && (-29LL - (long long )i) + (long long )size >= 0LL) && (29LL + (long long )i) - (long long )size >= 0LL) && (35LL - (long long )i) - (long long )size >= 0LL) && i == 3)) || (((((-35LL + (long long )i) + (long long )size >= 0LL && (-29LL - (long long )i) + (long long )size >= 0LL) && (29LL + (long long )i) - (long long )size >= 0LL) && (35LL - (long long )i) - (long long )size >= 0LL) && i == 3)) || (((((-34LL + (long long )i) + (long long )size >= 0LL && (-30LL - (long long )i) + (long long )size >= 0LL) && (30LL + (long long )i) - (long long )size >= 0LL) && (34LL - (long long )i) - (long long )size >= 0LL) && i == 2)) || (((((-34LL + (long long )i) + (long long )size >= 0LL && (-30LL - (long long )i) + (long long )size >= 0LL) && (30LL + (long long )i) - (long long )size >= 0LL) && (34LL - (long long )i) - (long long )size >= 0LL) && i == 2)) || (((((-33LL + (long long )i) + (long long )size >= 0LL && (-31LL - (long long )i) + (long long )size >= 0LL) && (31LL + (long long )i) - (long long )size >= 0LL) && (33LL - (long long )i) - (long long )size >= 0LL) && i == 1)) || (((((-33LL + (long long )i) + (long long )size >= 0LL && (-31LL - (long long )i) + (long long )size >= 0LL) && (31LL + (long long )i) - (long long )size >= 0LL) && (33LL - (long long )i) - (long long )size >= 0LL) && i == 1)) || ((((((-32LL + (long long )i) + (long long )size >= 0LL && (-32LL - (long long )i) + (long long )size >= 0LL) && (32LL + (long long )i) - (long long )size >= 0LL) && (32LL - (long long )i) - (long long )size >= 0LL) && 0 == i) && i == 0)) || ((((((-32LL + (long long )i) + (long long )size >= 0LL && (-32LL - (long long )i) + (long long )size >= 0LL) && (32LL + (long long )i) - (long long )size >= 0LL) && (32LL - (long long )i) - (long long )size >= 0LL) && 0 == i) && i == 0)) || ((((2147483616LL + (long long )i) + (long long )size >= 0LL && (2147483615LL - (long long )i) + (long long )size >= 0LL) && (2147483680LL + (long long )i) - (long long )size >= 0LL) && (2147483679LL - (long long )i) - (long long )size >= 0LL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 28 column: 5 function: main value: (((((((((((((((((((((((((((((((((((((((((((((((((((i == 7 || i == 21) || i == 6) || i == 20) || i == 6) || i == 20) || i == 5) || i == 19) || i == 5) || i == 19) || i == 4) || i == 18) || i == 4) || i == 18) || i == 3) || i == 17) || i == 3) || i == 17) || i == 2) || i == 16) || i == 2) || i == 16) || i == 1) || i == 15) || i == 1) || i == 15) || (0 == i && i == 0)) || i == 14) || (0 == i && i == 0)) || i == 14) || 8 <= i) || i == 13) || i == 13) || i == 12) || i == 12) || i == 11) || 25 <= i) || i == 11) || (25 <= i && i != 1)) || i == 10) || i == 24) || i == 10) || i == 24) || i == 9) || i == 23) || i == 9) || i == 23) || i == 8) || i == 22) || i == 8) || i == 22) || i == 7) || i == 21 format: c_expression | correctness_witness | CPAchecker 2.3 | 19 | 2023-12-01T04:45:12+01:00 |
Found 45 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0edf89e | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T06:37:04+01:00 | ||
6097c36 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T14:55:09Z | ||
8e6d6fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T14:51:24+01:00 | ||
508b873 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-12T01:54:56+01:00 | ||
01e7c4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2022-12-09T02:55:12+01:00 | ||
de42eac | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T17:25:44Z | ||
005ce1e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T23:13:31Z | ||
16fbe37 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:17:43Z | ||
80c646a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T03:06:26+01:00 | ||
f89c718 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 12 | 2022-12-14T12:30:38Z | ||
b8adef2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:19:52Z | ||
56c20c1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 738 | 2022-12-08T11:43:26+01:00 | ||
18e6c25 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 12 | 2022-12-13T13:51:15Z | ||
9b5377b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 8 | 2023-01-28T04:00:30+01:00 | 26d4730 | |
41f5966 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T21:59:48+01:00 | ||
924182a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:00:24Z | ||
3e3f079 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:01 CET (comp) | ||
c6da006 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 13 | 2022-12-14T07:33:14Z | ||
acf6f8d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T10:34:27Z | ||
45cf419 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T12:27:16Z | ||
30f8cbf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T17:42:25 | ||
59c063e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T10:55:57Z | ||
986fb06 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 7.0.0 kind | 3 | 2022-12-18T18:23:52Z | ||
3f4fb99 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 6.8.0 kind | 3 | 2022-12-25T10:34:27Z | ||
822ed56 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T10:51:26+01:00 | c6da006 | |
a15751a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 10 | 2023-01-29T07:40:19+01:00 | d56c34a | |
53ea7bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T05:21:28+01:00 | 45cf419 | |
70da0bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T04:48:58+01:00 | 30f8cbf | |
fcbb613 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:53:43+01:00 | 41f5966 | |
bd0619c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T17:38:45+01:00 | 924182a | |
ea1fd5c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T15:02:28+01:00 | 986fb06 | |
4b02a06 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T00:31:06+01:00 | 3f4fb99 | |
7193de8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-27T23:43:46+01:00 | 1f13984 | |
c2939d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T19:57:25+01:00 | ||
d15c81c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-12T02:48:25+01:00 | ||
d5f1296 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T04:36:17+01:00 | ||
26d4730 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CBMC | 725 | 2022-12-08T04:58:58+01:00 | ||
1f13984 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Bubaak | 3 | 2022-12-08T15:06:46Z | ||
d56c34a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 13 | 2022-12-13T14:20:38Z | ||
3f4791f | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T10:19:43Z | ||
9e23e99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T22:54:42Z | ||
6b27a80 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T10:50:03Z | ||
2bfe11d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2022-12-11T16:49:36 | ||
b53c04d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 725 | 2022-12-08T03:16:09+01:00 | ||
65359b5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T14:28:35Z |
Found 16 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9c04e47 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2021-12-07T08:04:28+01:00 | ||
4e2faf5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T17:04:59Z | ||
812d5e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-05T15:27:30+01:00 | ||
5314b2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 7 | 2021-12-08T20:32:00+01:00 | ||
3a50ff4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2021-12-09T10:51:34+01:00 | ||
4416398 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2021-12-07T02:30:06+01:00 | ||
d47eabd | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T03:45:54Z | ||
b567782 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 12 | 2021-12-10T06:05:33Z | ||
a8d2083 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 738 | 2021-12-06T09:29:07+01:00 | ||
44aadde | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 12 | 2021-12-06T22:54:22Z | ||
4f07c61 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 2 | 2021-12-06T11:54:55+01:00 | ||
6e1274a | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T09:37:21Z | ||
ff16b15 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | VERIFUZZ | 3 | 2021-12-11T10:46:25Z | ||
3456117 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T15:34:52Z | ||
b00a907 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2021-12-09T07:20:52 | ||
7e14882 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 725 | 2021-12-06T06:42:52+01:00 |
Found 8 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a0a6c50 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2020-12-06T18:30:10+01:00 | ||
231e188 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:56:31 | ||
a3c9be4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T15:25:59 | ||
57e6bcb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-05T14:31:18+01:00 | ||
e1f70f0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2020-12-08T02:11:38+01:00 | ||
1c6d74b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T14:39:44 | ||
67b8e19 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T18:47:12 | ||
71bfa58 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2020-12-08T09:38:29 |
Found 3 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
91ffeaa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-11-30T11:04:04+01:00 | ||
7b30e3a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 7 | 2019-12-01T02:23:33+01:00 | ||
f759504 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:22 CET (comp) |
Found 5 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c584fc3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:27 CET (sv-comp) | ||
e3bddb2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-05T09:48:23+01:00 | ||
0ba100e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-06T21:45:10+01:00 | ||
dc84801 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T20:19 CET (sv-comp) | ||
5dce3d7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:00 CET (sv-comp) |
Found 14 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
594d7e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:54 CET (sv-comp) | ||
6eb35a5 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:41:46.829647 | ||
8628189 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:31:37.050062 | ||
62ed6ce | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T08:34:31+01:00 | ||
7c972ed | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 9 | 2017-12-03T06:53Z | ||
a386552 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Map2Check | 4 | 2017-12-01T23:35 CET (sv-comp) | ||
2f05e0c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 838 | 2017-12-01T08:30 CET (sv-comp) | ||
cf549f0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 9 | 2017-12-03T03:59Z | ||
38a60fd | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 17 | 2017-12-01T08:23 CET (sv-comp) | ||
c6adaab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T22:37:21.502806 | ||
b5f627d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:43:44.535682 | ||
a7d628f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 272 | 2017-12-01T19:54 CET (sv-comp) | ||
a01e759 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 823 | 2017-12-01T13:26 CET (sv-comp) | ||
2dce131 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 16 | 2017-12-01T12:04 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |