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).
Key | Value |
programName | sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c |
programSHA | d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc |
witnessName | results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-memsafety.scopes4_false-valid-deref.c.files/witness.graphml |
witnessSHA | eb669f670a8ebfcec8b2bcc08331b2e82366f71d47d9216fe7985efb1a2b66d8 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T15:03Z |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | Taipan |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_5697df12-9d93-4d52-8397-913dd3849af6/sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c |
programhash | 25981771a012eec333f97d8302486eae22970d9e |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/eb669f670a8ebfcec8b2bcc08331b2e82366f71d47d9216fe7985efb1a2b66d8.graphml |
witness-sha256 | eb669f670a8ebfcec8b2bcc08331b2e82366f71d47d9216fe7985efb1a2b66d8 |
witness-size | 5969 |
witness-type | violation_witness |
Found 33 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
18bfec6 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:12:15+01:00 | ||
31ab53c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T23:02:07Z | ||
c8f30e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:25:56+01:00 | eabbf81 | |
e3a9b0d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:06:38+01:00 | 18bfec6 | |
5da80ea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-18T03:09:52+01:00 | 4b31dba | |
ee758e1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-17T22:08:35+01:00 | f2e614a | |
ad06200 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-05T14:37:34+01:00 | 21f5f89 | |
2946cf5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T16:44:29+01:00 | 7201ccc | |
9f2d0be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T12:12:03+01:00 | c0e2c90 | |
29ae3dd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:26:38+01:00 | 03e6d76 | |
30a4c00 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T06:19:04+01:00 | c42dcf1 | |
07988e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T22:55:56+01:00 | 350b70b | |
17b0c54 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:27:06+01:00 | 7fcd802 | |
eb20d32 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:42:37+01:00 | 93765c0 | |
66caa26 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T09:44:20+01:00 | 5c1ee3c | |
93765c0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-11-30T07:12:46+01:00 | ||
57932b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T03:02:39+01:00 | 31ab53c | |
42898e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:32:13+01:00 | 2cc2c3a | |
5139709 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-28T23:49:48+01:00 | 04ef0f0 | |
03e6d76 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-03T23:08:11+01:00 | ||
eabbf81 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-19T01:14:02+01:00 | ||
4b31dba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2023-12-18T02:16:01+01:00 | ||
7fcd802 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T14:27:36Z | ||
c0e2c90 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 6 | 2023-12-02T16:41:13Z | ||
c42dcf1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 6 | 2023-12-02T21:12:23Z | ||
f2e614a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 4 | 2023-12-17T10:30:05+01:00 | ||
2cc2c3a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 6 | 2023-11-28T23:48:29Z | ||
04ef0f0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T20:11:57Z | ||
5c1ee3c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:25:43Z | ||
21f5f89 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T10:57:02Z | ||
7201ccc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T14:59:41Z | ||
350b70b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T21:10:14Z | ||
63ae9d7 | Inspect | - content: - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4d83a3bc-572a-4af9-940d-3c264ae7a2b7/sv-benchmarks/c/memsafety-ext3/scopes4-2.c line: 18 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:02:07Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4d83a3bc-572a-4af9-940d-3c264ae7a2b7/sv-benchmarks/c/memsafety-ext3/scopes4-2.c : d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4d83a3bc-572a-4af9-940d-3c264ae7a2b7/sv-benchmarks/c/memsafety-ext3/scopes4-2.c language: C specification: CHECK( init(main()), LTL(G valid-free) ),CHECK( init(main()), LTL(G valid-deref) ),CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T02:58:37+01:00 |
Found 27 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
22f0472 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:30:39+01:00 | ||
102c948 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T14:00:25Z | ||
de73850 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T10:44:47+01:00 | 47b3227 | |
8b2b68e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:53:31+01:00 | de5b679 | |
c4ff093 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:38:31+01:00 | a7429b3 | |
b46eadc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T05:55:46+01:00 | 102c948 | |
832b208 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T04:19:15+01:00 | d14d961 | |
0943445 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T01:32:24+01:00 | 9b59f5c | |
9768dfb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:05:05+01:00 | a09b410 | |
907bee3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:41:38+01:00 | 2d1c06d | |
662f547 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:20:07+01:00 | 22f0472 | |
1f958dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:57:42+01:00 | ea52133 | |
6a425f2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T06:00:58+01:00 | cc20063 | |
8469938 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T04:24:00+01:00 | 4bbe49c | |
b15f600 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:20:05+01:00 | 036ba29 | |
4fe0957 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:28:50+01:00 | e94a32e | |
ea52133 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2022-12-10T15:12:35+01:00 | ||
9b59f5c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-12T01:52:03+01:00 | ||
cc20063 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2022-12-09T02:36:15+01:00 | ||
2d1c06d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T19:19:43Z | ||
036ba29 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T09:49:05Z | ||
a09b410 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-10T02:17:15+01:00 | ||
47b3227 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 6 | 2022-12-14T05:16:57Z | ||
a7429b3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 6 | 2022-12-14T20:29:20Z | ||
4bbe49c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 4 | 2022-12-08T12:01:09+01:00 | ||
de5b679 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 6 | 2022-12-13T13:11:17Z | ||
e94a32e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T17:43:14Z |
Found 26 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
debde86 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T10:00:20+01:00 | ||
ede715c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:21:23 | ||
a8acf94 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T09:15:46Z | ||
7d92df6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-10T21:26:50+01:00 | 89239ca | |
b059b6a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-10T17:27:29+01:00 | 176b3a8 | |
90948ad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-10T08:34:04+01:00 | b71a484 | |
450acdc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-09T16:01:05+01:00 | 6e1aa38 | |
1222f4d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-09T06:21:16+01:00 | d14d961 | |
c069663 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-08T21:11:18+01:00 | d957050 | |
dc9001f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-08T13:48:38+01:00 | 77d8030 | |
68241b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T19:13:16+01:00 | a8acf94 | |
7604b02 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T11:27:06+01:00 | debde86 | |
367231a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T04:55:13+01:00 | cc5a214 | |
21941f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T02:36:39+01:00 | 4745e4c | |
358802f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-06T11:48:33+01:00 | 9e49a6e | |
91dde5e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-05T20:38:33+01:00 | 1813fda | |
1813fda | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-05T18:29:03+01:00 | ||
6e1aa38 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T10:20:21+01:00 | ||
cc5a214 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2021-12-07T01:53:01+01:00 | ||
77d8030 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T04:06:58Z | ||
d957050 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T18:59:30+01:00 | ||
b71a484 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 6 | 2021-12-10T03:58:32Z | ||
176b3a8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 6 | 2021-12-10T12:21:18Z | ||
9e49a6e | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 4 | 2021-12-06T09:25:10+01:00 | ||
4745e4c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 6 | 2021-12-06T20:46:03Z | ||
af55d90 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 2 | 2021-12-06T11:19:17+01:00 |
Found 17 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7759639 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:22:50+01:00 | ||
a675c93 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T20:53:45 | ||
6522d84 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T16:33:50 | ||
0ae3b39 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-12T01:35:48+01:00 | a675c93 | |
da5cefb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T22:12:12+01:00 | 9567497 | |
a9e017e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-07T16:47:26+01:00 | a7a712b | |
5324fbc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T18:28:19+01:00 | 4fe2c3a | |
6b14837 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-05T18:11:33+01:00 | 4fc67a8 | |
4fc67a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-05T15:08:53+01:00 | ||
55288ed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T00:51:35+01:00 | ||
9e799b9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T04:06:23+01:00 | 6522d84 | |
6ee5cec | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T02:24:25+01:00 | fb393c5 | |
fbed790 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-08T07:31:51+01:00 | 55288ed | |
5d9b59d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T19:13:01+01:00 | 7759639 | |
02f5a29 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T21:31:14+01:00 | 719cd80 | |
58cc343 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T18:01:35+01:00 | 4fc67a8 | |
f9019f9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T07:39:37+01:00 | 4fe2c3a |
Found 13 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0e8c7fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-02 05:34:40 | ||
52ea798 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:56:37+01:00 | a699f5c | |
2eafca8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:09:15+01:00 | 0e8c7fb | |
8458db4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T20:54:19+01:00 | 70f6cba | |
2d8b0e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-08T00:06:01+01:00 | d14d961 | |
7a9feff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-07T21:15:01+01:00 | a8db258 | |
5e8f1a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-05T20:20:12+01:00 | 059bb18 | |
aa10d0c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-03T08:57:39+01:00 | 00f311f | |
510bd55 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-11-29T21:12:04+01:00 | ||
b53bbfa | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:41:46+01:00 | bb2dca1 | |
bb2dca1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T01:55:54+01:00 | ||
a2e8e61 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-08T00:26:02+01:00 | 75f6c1e | |
48757d8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-03T08:28:56+01:00 | 510bd55 |
Found 14 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0db4660 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T09:17 CET (sv-comp) | ||
a94ccea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:53:14+01:00 | eb669f6 | |
d249db3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:38:25+01:00 | 3bb1c31 | |
8e05208 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T08:35:44+01:00 | 9b9e070 | |
367c4e1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:48:52+01:00 | 0b02eaf | |
9cab106 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:01:44+01:00 | eee5b66 | |
5dea50f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:44+01:00 | d0624fb | |
ad701c2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:44:41+01:00 | 0db4660 | |
1d896f9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T09:25:03+01:00 | d90c59b | |
9b9e070 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-08T04:19:51+01:00 | ||
dd45059 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:21:47+01:00 | 0094f48 | |
01c14cb | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:05:23+01:00 | d0624fb | |
70d91c5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:12:00+01:00 | ce93676 | |
0b02eaf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T02:09:09+01:00 |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_false-valid-deref.c, d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d3e64a3bb1136adaedbe48fbb8a8a2a2e8de15e4ab22e021abc9c36f399fb6cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |