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/array-memsafety/mult_array_unsafe_false-valid-deref.i |
programSHA | f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4 |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-memsafety.mult_array_unsafe_false-valid-deref.i.files/witness.graphml |
witnessSHA | 56d614d0716be6ae48cffb2a620859f75265fe0a0bbcd41b6327ec5285285b00 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T05:47 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_d563a018-a2a8-4b46-b026-fd7ddbe1d218/sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i |
programhash | f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/56d614d0716be6ae48cffb2a620859f75265fe0a0bbcd41b6327ec5285285b00.graphml |
witness-sha256 | 56d614d0716be6ae48cffb2a620859f75265fe0a0bbcd41b6327ec5285285b00 |
witness-size | 1793 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
56d614d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2018-12-08T05:47 CET (sv-comp) | ||
10c2e43 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:44:06+01:00 | 56d614d | |
8fab2a1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:07:24+01:00 | 55e9f11 | |
288ca67 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T05:02:49+01:00 | 708dab9 | |
5d37338 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-07T05:24:36+01:00 | ||
a2c825f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:25:55+01:00 | e7f0f82 | |
3b33ccd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T07:49:00+01:00 | ||
55e9f11 | Inspect | 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 | 4 | 2018-12-08T16:15:40 | ||
d44d89c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:53:11+01:00 | 227b562 | |
f1402a6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:37:01+01:00 | cb2a68a | |
bf326e5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:20:30+01:00 | bbc03f4 | |
ef5c511 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T10:20:14+01:00 | 66bb206 | |
02efeae | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:16:56+01:00 | 97d587b |
Found 9 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
445c721 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2017-12-02T23:50 CET (sv-comp) | ||
68d12ce | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:33:20.070063 | ||
cae3ac7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:42:39.213298 | ||
454608f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:40 CET (sv-comp) | ||
197dc38 | 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 | 7 | 2017-12-03T06:53Z | ||
ba6bb3e | 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 | 7 | 2017-12-03T04:25Z | ||
4e69ddf | 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 | 7 | 2017-12-01T08:29 CET (sv-comp) | ||
836ceb8 | 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 | 7 | 2017-12-03T03:48Z | ||
a2cb049 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:50 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/mult_array_unsafe_false-valid-deref.i, f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f26f7502c1a8aa7f2988aceee3d6c7c1efb2dcf250d4e5e825fce63b11142cb4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |