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/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i |
programSHA | 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc |
witnessName | results-verified/predatorhp.2017-12-01_2145.logfiles/sv-comp18.memleaks_test13_1_false-valid-memtrack_true-termination.i.files/witness.graphml |
witnessSHA | 5c50dfabc35b40531bb727e90a233a5d572d1ae10e68ec350f6412d8277d946e |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T22:08 CET (sv-comp) |
memorymodel | precise |
producer | PredatorHP |
program-sha256 | 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc |
programfile | ../../sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i |
programhash | ba5476636e8902440a35b69190524704fd5af5c4 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/5c50dfabc35b40531bb727e90a233a5d572d1ae10e68ec350f6412d8277d946e.graphml |
witness-sha256 | 5c50dfabc35b40531bb727e90a233a5d572d1ae10e68ec350f6412d8277d946e |
witness-size | 4562 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e526ee1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T12:41 CET (sv-comp) | ||
0ee13f6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-08T03:45:19+01:00 | ||
5a4258b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T23:44:33+01:00 | e526ee1 | |
3f2af73 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T22:11:26+01:00 | 3cd4f86 | |
da7e548 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:41:49+01:00 | c3e35f9 | |
27455ed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T04:51:20+01:00 | 7031dbd | |
03b16a2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T09:19:42+01:00 | b490f91 | |
992b04a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T07:53:30+01:00 | 0ee13f6 | |
ce788df | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T09:15:07+01:00 | 5c50dfa | |
bbb0bde | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T02:35:28+01:00 | ||
334ca70 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T10:14:09+01:00 | 7bc7298 | |
3cd4f86 | 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 | 3 | 2018-12-08T08:19:54 | ||
39d1a42 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T01:05:56+01:00 | 8301e66 | |
48ee4a0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:48:18+01:00 | bbb0bde | |
a239279 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:15 CET (sv-comp) | ||
b4ef082 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:06 CET (sv-comp) |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
352768d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:23 CET (sv-comp) | ||
5c50dfa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 5 | 2017-12-01T22:08 CET (sv-comp) | ||
8ce0cb5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:53 CET (sv-comp) | ||
906c021 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T08:23:22+01:00 | ||
c88bbcb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:53:24.710261 | ||
6c1c576 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:10:03.230376 | ||
df7fb10 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:30 CET (sv-comp) | ||
10ddb69 | 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 | 13 | 2017-12-01T08:22 CET (sv-comp) | ||
01efc8b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 4 | 2017-12-01T08:19 CET (sv-comp) | ||
40ccb30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T22:55:38.550367 | ||
e08d513 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:15:30.802271 | ||
8029903 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 8 | 2017-12-01T17:23 CET (sv-comp) | ||
ec2d474 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 9 | 2017-12-01T17:36 CET (sv-comp) | ||
7616f16 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 24 | 2017-12-01T17:03 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i, 3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3f2c6d4a149818da1f8a4a34a5411c85420fc94c0cf0902e5231224edcfbc3dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |