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/count_down_unsafe_false-valid-deref.i |
programSHA | e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-memsafety.count_down_unsafe_false-valid-deref.i.files/witness.graphml |
witnessSHA | 2fc9a65212543efbbf89f8f2a2e4092fdd5927ed86ecee26ea058dd73dcd2983 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T22:33:27+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb |
programfile | ../../sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i |
programhash | e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/2fc9a65212543efbbf89f8f2a2e4092fdd5927ed86ecee26ea058dd73dcd2983.graphml |
witness-sha256 | 2fc9a65212543efbbf89f8f2a2e4092fdd5927ed86ecee26ea058dd73dcd2983 |
witness-size | 7683 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e8face3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2018-12-08T09:36 CET (sv-comp) | ||
1dd14b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:38:04+01:00 | 28a51cf | |
bb0b8f1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:09:54+01:00 | 1dfa183 | |
d010c4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:17:25+01:00 | d3f4480 | |
84e9549 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:28:44+01:00 | 7e1aff6 | |
2fc9a65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-05T22:33:27+01:00 | ||
2bb66d1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:17:30+01:00 | 1ce6692 | |
626d420 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T09:22:20+01:00 | 5da9325 | |
1dfa183 | 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-07T20:19:50 | ||
7f7d860 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:53:23+01:00 | 2e27efb | |
8daac56 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:41:57+01:00 | e8face3 | |
e863507 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T05:03:48+01:00 | 5102311 | |
820359f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:17:05+01:00 | 9c547a2 | |
92204e1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-08T02:52:28+01:00 |
Found 9 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ec09287 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2017-12-03T00:12 CET (sv-comp) | ||
e6ad731 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T12:00:08.901539 | ||
41eee8b | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:14:18.628589 | ||
f1ccae6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:21 CET (sv-comp) | ||
ee62e35 | 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 | ||
506b3f7 | 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 | 2017-12-03T04:26Z | ||
4dd1d2c | 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 | 5 | 2017-12-01T08:21 CET (sv-comp) | ||
6c8f1c1 | 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 | 2017-12-03T04:14Z | ||
ed18f87 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:22 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |