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/derefAfterFree1_false-valid-deref.c
programSHA a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670
witnessName results-validated/cpa-seq-validate-violation-witnesses-esbmc-kind.2018-12-08_0449.logfiles/sv-comp19_prop-memsafety.derefAfterFree1_false-valid-deref.c.files/witness.graphml
witnessSHA 9bc27ecb4127ffb7565ba35bca849e5fda90a00a60e25ff01892c626e97ddf08

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T04:57:09+01:00
inputwitnesshash 87fb153b08665108c70aaad489a0c667fa13ff24d18c401b52ed8b5c8e318f08
producer CPAchecker 1.7-svn 29852
program-sha256 a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670
programfile ../../sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c
programhash a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/9bc27ecb4127ffb7565ba35bca849e5fda90a00a60e25ff01892c626e97ddf08.graphml
witness-sha256 9bc27ecb4127ffb7565ba35bca849e5fda90a00a60e25ff01892c626e97ddf08
witness-size 3644
witness-type violation_witness

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

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 87f9be9 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:59:41+01:00
Download af15139 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T19:00:30Z
Download 90d909a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-19T05:27:52+01:00 Download 1465b70
Download 1512f41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-18T12:05:42+01:00 Download 87f9be9
Download bcecead Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-18T03:09:33+01:00 Download 3076dda
Download 03b939d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-17T22:07:24+01:00 Download ab58eca
Download bac4f58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-05T14:37:50+01:00 Download 152187e
Download 7fa5f27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-04T16:46:17+01:00 Download ac8d3f9
Download c47b271 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-04T12:12:19+01:00 Download 6348dc4
Download 332811f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-04T02:27:20+01:00 Download 8ecf46d
Download 40e80f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-03T06:18:56+01:00 Download a04a087
Download 4901a18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-01T22:54:34+01:00 Download f750186
Download e935239 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-12-01T18:28:31+01:00 Download 34aeb70
Download a41fbd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T13:42:53+01:00 Download b525cfe
Download 6cb6674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T09:44:11+01:00 Download 1fba2c7
Download b525cfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T07:01:06+01:00
Download bd9b960 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T03:05:27+01:00 Download af15139
Download a00d526 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-29T08:32:49+01:00 Download ef87d66
Download 87c4f78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-28T23:49:52+01:00 Download 78f9630
Download 8ecf46d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T23:47:33+01:00
Download 3076dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2023-12-18T01:58:53+01:00
Download 34aeb70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T12:53:33Z
Download 6348dc4 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 5 2023-12-02T18:40:28Z
Download a04a087 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 5 2023-12-03T01:47:14Z
Download ab58eca 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 3 2023-12-17T20:33:16+01:00
Download ef87d66 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 5 2023-11-28T22:55:35Z
Download 78f9630 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T20:38:16Z
Download 1fba2c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:24:28Z
Download 1465b70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T17:08:38+01:00
Download 152187e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T11:42:30Z
Download ac8d3f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T10:08:18Z
Download f750186 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:53:05Z
Download 8e95945 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_deac57f0-a087-43f0-bb3e-6c132c1e8ca4/sv-benchmarks/c/memsafety-ext3/derefAfterFree1.c line: 14 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:00:30Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_deac57f0-a087-43f0-bb3e-6c132c1e8ca4/sv-benchmarks/c/memsafety-ext3/derefAfterFree1.c : a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_deac57f0-a087-43f0-bb3e-6c132c1e8ca4/sv-benchmarks/c/memsafety-ext3/derefAfterFree1.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 5 2023-11-30T03:00:14+01:00

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 65d4852 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:36:05+01:00
Download d8d84fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T16:43:27Z
Download e3bca3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-29T10:45:42+01:00 Download 98427e6
Download 51285db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-29T06:53:03+01:00 Download a4eaaa2
Download 7dd101a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-29T06:38:23+01:00 Download 0fb91db
Download 11c9c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-29T05:57:38+01:00 Download d8d84fb
Download af5c3f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-29T04:19:13+01:00 Download 1532656
Download ddd4ead Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-29T01:32:27+01:00 Download 856eea7
Download c00744f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T21:05:18+01:00 Download 7eb4fc3
Download e525116 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T15:45:12+01:00 Download 8fc4e75
Download 0190e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T14:14:43+01:00 Download 65d4852
Download fe28e44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T08:57:58+01:00 Download 689c97d
Download 0e35044 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T06:01:33+01:00 Download 1665708
Download dc49988 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T04:24:02+01:00 Download 51c8681
Download 74bf977 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T02:22:38+01:00 Download 3a8ec6a
Download 4ee9f26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 4 2023-01-28T00:29:08+01:00 Download 9b46827
Download 689c97d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T16:10:08+01:00
Download 856eea7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-11T19:37:57+01:00
Download 1665708 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2022-12-09T03:27:02+01:00
Download 8fc4e75 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:04:42Z
Download 3a8ec6a 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:34:17Z
Download 7eb4fc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T00:33:51+01:00
Download 98427e6 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 5 2022-12-14T13:45:09Z
Download 0fb91db 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 5 2022-12-14T20:01:20Z
Download 51c8681 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 3 2022-12-08T05:52:12+01:00
Download a4eaaa2 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 5 2022-12-13T17:59:40Z
Download 9b46827 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T15:47:11Z

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

Found 27 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c, a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a9913d8 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:08:24+01:00
Download 03a3379 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:03:12
Download f1946d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T10:18:53Z
Download f2c749d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-10T21:28:14+01:00 Download cc02325
Download 667d8f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-10T17:27:33+01:00 Download c6f45bd
Download 2d46e50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-10T08:33:56+01:00 Download 17ecc7c
Download 5e6b5dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-09T16:03:02+01:00 Download 0a04573
Download bb88e71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-09T06:21:56+01:00 Download 1532656
Download 8bcfa7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-08T21:11:27+01:00 Download a0bf40f
Download 9f44236 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-08T13:49:03+01:00 Download 1c6febb
Download a164f02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-07T19:11:31+01:00 Download f1946d3
Download 8ce6708 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-07T11:27:34+01:00 Download a9913d8
Download b8e6a5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-07T04:55:08+01:00 Download 48ff8f6
Download 862dbda Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-07T02:36:57+01:00 Download cbc5156
Download facd8b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-06T12:47:27+01:00 Download 99ca683
Download 386224b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-06T11:48:19+01:00 Download e4f9971
Download 7b8e9d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 4 2021-12-05T20:41:39+01:00 Download b92d4cb
Download b92d4cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T14:47:19+01:00
Download 0a04573 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T11:29:40+01:00
Download 48ff8f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2021-12-07T03:33:44+01:00
Download 1c6febb 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:30:42Z
Download 17ecc7c 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 5 2021-12-10T01:52:22Z
Download c6f45bd 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 5 2021-12-10T14:37:11Z
Download e4f9971 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 2021-12-06T07:54:40+01:00
Download cbc5156 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 5 2021-12-06T20:47:01Z
Download 99ca683 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:31:53+01:00
Download a0bf40f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T20:34:12+01:00

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 317bf2d Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:16:22+01:00
Download 73681ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T21:08:13
Download d65b1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T19:30:18
Download 65087ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 4 2020-12-09T22:06:14+01:00 Download 76eb8b2
Download 823df97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 4 2020-12-07T17:01:04+01:00 Download 50b44da
Download 795aa32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 4 2020-12-06T18:25:05+01:00 Download e04523b
Download 245d6fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 4 2020-12-06T18:02:12+01:00 Download db4eaa0
Download 541caa2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 4 2020-12-05T18:13:23+01:00 Download db4eaa0
Download db4eaa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T13:16:29+01:00
Download 2d304bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-07T22:41:56+01:00
Download 8f7d165 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 4 2020-12-09T21:49:14+01:00 Download c62d35d
Download 913445e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 4 2020-12-06T19:17:39+01:00 Download 317bf2d
Download 5f07873 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 4 2020-12-12T01:30:41+01:00 Download 73681ed
Download 2bdfe1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 4 2020-12-09T04:09:19+01:00 Download d65b1b5
Download 78436b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 4 2020-12-09T02:09:29+01:00 Download 5764c99
Download 888b5b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 4 2020-12-08T07:30:03+01:00 Download 2d304bb
Download e53cf9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 4 2020-12-06T07:47:12+01:00 Download e04523b

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eaea592 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 04:55:57
Download 40cb5b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 4 2019-12-11T21:09:07+01:00 Download eaea592
Download 9da84a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 4 2019-12-11T20:54:45+01:00 Download 8e43d0c
Download 5563cff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 4 2019-12-07T21:17:03+01:00 Download 33c294e
Download 6cfb253 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 4 2019-12-03T08:10:17+01:00 Download a34d18b
Download 67f7371 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T15:45:20+01:00
Download 4238fe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 4 2019-12-11T21:55:20+01:00 Download 67f7371
Download e6436bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 4 2019-12-11T21:44:48+01:00 Download 3c9617f
Download 13d7e6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 4 2019-12-05T20:20:24+01:00 Download 55a40f3
Download a34d18b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-11-30T00:48:22+01:00
Download 461ae00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 3 2019-12-03T08:56:45+01:00 Download a90ccdb
Download 809ccd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 4 2019-12-08T00:27:11+01:00 Download 41b43c2
Download 67b5db3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 4 2019-12-08T00:06:03+01:00 Download 1532656

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0f85474 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T04:49 CET (sv-comp)
Download cd98b97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:53:16+01:00 Download 7f5b46f
Download 62d3640 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:20:18+01:00 Download 0f003eb
Download 9251c7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T08:28:28+01:00 Download 18aa017
Download 9bc27ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:57:09+01:00 Download 87fb153
Download 32099b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:48:41+01:00 Download 295026c
Download 295026c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-05T15:15:16+01:00
Download 28154de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:40:20+01:00 Download af46692
Download 0c70a8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-07T09:20:29+01:00 Download 90463df
Download 770e4b2 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-07T23:09:16
Download 18aa017 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T01:01:22+01:00
Download cde7760 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:48:58+01:00 Download 123c877
Download 7fb4c04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:42:08+01:00 Download 0f85474
Download 8d3e732 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T22:09:14+01:00 Download 770e4b2
Download 4446371 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:00:27+01:00 Download 123c877
Download e414b91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-07T01:19:24+01:00 Download 3d7de8d
Download 0aa050c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T10:18:23+01:00 Download 85d07a3
Download 34e47db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:19:25+01:00 Download ca5187a
Download e62bc10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:12:07+01:00 Download 0961857

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

Trying to find witnesses for program (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c, a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670.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 (a759f8d678ad469b9fde9b60c61d539be5ffd1b82a7250e29929fb245cee5670, sv-benchmarks/c/memsafety-ext3/derefAfterFree1_false-valid-deref.c).

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

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