Witness Inspection

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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c
programSHA 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
witnessName results-validated/cpa-seq-validate-violation-witnesses-utaipan.2018-12-09_2052.logfiles/sv-comp19_prop-memsafety.derefAfterFree2_false-valid-deref.c.files/witness.graphml
witnessSHA d453ac83d54e0b50b22378bb32dd8403357b46af52362b423ba8e583b6c743c0

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/d453ac83d54e0b50b22378bb32dd8403357b46af52362b423ba8e583b6c743c0.json

Key Value
architecture 32bit
creationtime 2018-12-09T20:53:09+01:00
inputwitnesshash 64851d5ff9a13304525ff9b0543f04a2f82d1e11f8c9f10e9462cb8e631cded2
producer CPAchecker 1.7-svn 29852
program-sha256 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
programfile ../../sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c
programhash 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/d453ac83d54e0b50b22378bb32dd8403357b46af52362b423ba8e583b6c743c0.graphml
witness-sha256 d453ac83d54e0b50b22378bb32dd8403357b46af52362b423ba8e583b6c743c0
witness-size 13307
witness-type violation_witness

This witness was created for this program (cf. table above, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5).

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 33 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aa899dd Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:59:45+01:00
Download aaf7c5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T19:06:40Z
Download 7d52494 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-19T05:25:42+01:00 Download e3f9174
Download b1f4d7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-18T12:06:44+01:00 Download aa899dd
Download 776c85c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-18T03:09:07+01:00 Download 58c427b
Download 37d2cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-17T22:06:24+01:00 Download 6c656ea
Download a337b13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-05T14:37:03+01:00 Download 455a3e6
Download 80b7047 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-04T16:43:07+01:00 Download 52e2c23
Download 40996b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-04T12:11:44+01:00 Download 8920c11
Download 2ee5b2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-04T02:26:08+01:00 Download 0402502
Download 4e52c83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-03T06:18:34+01:00 Download 727ff01
Download 589fc7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-01T22:56:15+01:00 Download 3f0e10e
Download 2c768dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-01T18:30:00+01:00 Download b814eeb
Download a83a78f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T13:42:52+01:00 Download 399e83c
Download eb668f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T09:44:05+01:00 Download 75fa13f
Download 399e83c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 11 2023-11-30T08:43:50+01:00
Download a637669 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T03:04:28+01:00 Download aaf7c5f
Download dc745cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-29T08:33:45+01:00 Download 5322957
Download 71e5891 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-28T23:49:34+01:00 Download 95671bf
Download 0402502 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 13 2023-12-03T20:32:52+01:00
Download e3f9174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 13 2023-12-18T23:53:55+01:00
Download 58c427b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 17 2023-12-18T01:34:01+01:00
Download b814eeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T14:11:39Z
Download 8920c11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 11 2023-12-02T18:59:12Z
Download 727ff01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 11 2023-12-02T23:50:59Z
Download 6c656ea Inspect Inspect
Validate
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-17T08:24:42+01:00
Download 5322957 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 11 2023-11-29T01:44:22Z
Download 95671bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T20:31:14Z
Download 75fa13f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 5 2023-11-30T08:25:40Z
Download 455a3e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T12:54:48Z
Download 52e2c23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T09:05:00Z
Download 3f0e10e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:53:44Z
Download bb35a15 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 9 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ee0282f-f1f9-4818-a0c1-c36196447bfc/sv-benchmarks/c/memsafety-ext3/derefAfterFree2.c line: 9 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:06:40Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ee0282f-f1f9-4818-a0c1-c36196447bfc/sv-benchmarks/c/memsafety-ext3/derefAfterFree2.c : 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ee0282f-f1f9-4818-a0c1-c36196447bfc/sv-benchmarks/c/memsafety-ext3/derefAfterFree2.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 14 2023-11-30T02:56:34+01:00

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 27 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3208831 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:33:59+01:00
Download 091d853 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T12:48:08Z
Download d4001a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T10:43:54+01:00 Download 7b52144
Download 3ee9fd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T06:53:24+01:00 Download f2bae41
Download 3691221 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T06:38:23+01:00 Download 9f0b106
Download e4c998a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T05:56:50+01:00 Download 091d853
Download 5d3f698 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T04:19:22+01:00 Download 7b0e2fb
Download 42c765c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T01:32:19+01:00 Download 4636906
Download 1ee8ab2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T21:06:33+01:00 Download 49a45db
Download 7a6032c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T15:42:10+01:00 Download 3135367
Download fa3646a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T14:11:29+01:00 Download 3208831
Download 8e77ffe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T08:58:37+01:00 Download c071e0d
Download 2a3225d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T06:01:34+01:00 Download 833947f
Download 7ba74ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T04:21:33+01:00 Download ab29dd1
Download 2e2c89a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T02:23:04+01:00 Download 0f12b85
Download 8c9eb52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T00:29:14+01:00 Download 27abf50
Download c071e0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2022-12-10T18:40:01+01:00
Download 4636906 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 13 2022-12-11T22:06:36+01:00
Download 49a45db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 13 2022-12-10T04:04:42+01:00
Download 833947f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 17 2022-12-09T03:22:22+01:00
Download 3135367 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T22:35:58Z
Download 0f12b85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T08:56:18Z
Download 7b52144 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 11 2022-12-14T07:42:13Z
Download 9f0b106 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 11 2022-12-14T19:27:46Z
Download ab29dd1 Inspect Inspect
Validate
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-08T05:38:01+01:00
Download f2bae41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 11 2022-12-13T18:07:08Z
Download 27abf50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T17:34:00Z

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 25 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bbb4d3b Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T10:03:41+01:00
Download 80b254c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T18:55:05
Download f7053a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T15:23:07Z
Download 139b830 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-10T21:26:16+01:00 Download 1ce47a4
Download 4252f15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-10T17:27:10+01:00 Download fd19d4a
Download b1b0b5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-10T08:33:28+01:00 Download a551d55
Download 43eb9a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-09T16:01:15+01:00 Download 1d7e16f
Download 54c01e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-09T06:21:17+01:00 Download 7b0e2fb
Download 71e4cd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-08T21:06:45+01:00 Download f9af772
Download 1b6898a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-08T13:47:26+01:00 Download 000877f
Download ed69e40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T19:12:22+01:00 Download f7053a1
Download a86ee0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T11:28:08+01:00 Download bbb4d3b
Download 117af65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T04:56:27+01:00 Download 753fa68
Download 7bfe807 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T02:36:39+01:00 Download 9395076
Download 9856b9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-06T11:48:26+01:00 Download 5c45e0f
Download 010edfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-05T20:40:34+01:00 Download 7c29257
Download 7c29257 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-05T17:45:41+01:00
Download f9af772 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 13 2021-12-08T17:43:38+01:00
Download 1d7e16f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 13 2021-12-09T12:05:59+01:00
Download 753fa68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 17 2021-12-07T02:08:42+01:00
Download 000877f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T11:07:18Z
Download a551d55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 11 2021-12-10T05:05:58Z
Download fd19d4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 11 2021-12-10T09:03:26Z
Download 5c45e0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 9 2021-12-06T03:16:08+01:00
Download 9395076 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 11 2021-12-06T18:19:15Z

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 17 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e9ddee0 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:57:25+01:00
Download e92d0a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T18:30:34
Download deb5ca3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T02:23:50
Download 0942250 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-12T01:34:54+01:00 Download e92d0a5
Download 8fe86a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-09T21:55:10+01:00 Download 9ffae74
Download 386c95d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-09T21:35:26+01:00 Download a738630
Download ae2c86b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-09T04:11:49+01:00 Download deb5ca3
Download 06560b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-09T01:44:40+01:00 Download 73f7078
Download 95a72e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-08T07:52:21+01:00 Download 63382bf
Download 2102eb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-07T16:55:49+01:00 Download fa0dadd
Download 71baf7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-06T18:28:10+01:00 Download bda7fcb
Download 93b6f87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-06T18:00:53+01:00 Download 1707387
Download 70c0e5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-06T07:51:14+01:00 Download bda7fcb
Download 87a7b0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-05T18:35:05+01:00 Download 1707387
Download 1707387 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-05T17:03:21+01:00
Download 63382bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 13 2020-12-07T22:53:21+01:00
Download bd8c043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 13 2020-12-06T19:13:31+01:00 Download e9ddee0

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 13 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 480af7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 06:29:40
Download 1d7aeb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 13 2019-12-11T21:46:32+01:00 Download 40d361c
Download 569ccd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 13 2019-12-11T21:09:17+01:00 Download 480af7e
Download da2ad4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 13 2019-12-08T00:27:19+01:00 Download f6bcf87
Download 742a2e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 13 2019-12-03T08:09:29+01:00 Download 8b4c232
Download 8b4c232 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 13 2019-11-30T10:19:39+01:00
Download 032f1f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-07T21:12:57+01:00 Download 2ecacd3
Download 2fab3a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-03T08:57:52+01:00 Download 6e20181
Download d0c984a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 5 2019-12-05T20:21:27+01:00 Download 8f686ff
Download 5429867 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-11T22:00:46+01:00 Download 49ec423
Download 8aa8690 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-11T20:55:14+01:00 Download 0397d4b
Download e9b026d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-08T00:07:31+01:00 Download 7b0e2fb
Download 40d361c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 13 2019-12-01T00:25:37+01:00

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 19 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 828b3ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T02:18 CET (sv-comp)
Download 11542f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:48:40+01:00 Download c8d1c29
Download d453ac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:53:09+01:00 Download 64851d5
Download 40a60dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T22:07:37+01:00 Download ea8a462
Download 17df607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T07:43:43+01:00 Download e3f9ce6
Download 8160fbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T03:41:17+01:00 Download c8d1c29
Download f961cc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-07T09:17:17+01:00 Download 26c2ab4
Download e7b3a73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:16:54+01:00 Download 60f1df6
Download ea8a462 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness SMACK 1.9.3 3 2018-12-08T10:24:27
Download e3f9ce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-08T00:50:45+01:00
Download 11a0af1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:38:29+01:00 Download fb074f6
Download bfd27b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:22:12+01:00 Download 787c806
Download e29602f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T23:43:59+01:00 Download 828b3ae
Download ff52a83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T05:03:22+01:00 Download c36a716
Download 5c2f9db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-07T01:15:52+01:00 Download 6736b60
Download 701c750 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-06T10:15:11+01:00 Download 79133ce
Download 8380bea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:48:52+01:00 Download 4aaad98
Download 4aaad98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-05T12:28:14+01:00
Download 3e07b82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:00:28+01:00 Download f15ded6

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5, sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness