cd8cac2 |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2023-12-18T11:01:37+01:00 |
|
ab4bf4a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-16T23:00:26Z |
|
c48b332 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-18T12:06:51+01:00 |
cd8cac2 |
62ef750 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T06:10:04+01:00 |
|
31d4c83 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T23:22:15+01:00 |
|
8bd5be4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
7 |
2023-12-19T12:58:24+01:00 |
|
50bda01 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
12 |
2023-12-18T02:19:50+01:00 |
|
8acf2ba |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Automizer |
15 |
2023-11-29T01:40:25Z |
|
6a65620 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-18T18:53:08+01:00 |
|
1dd18bd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:24:12+01:00 |
|
29f958f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T08:02:45Z |
|
ef2678b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
15 |
2023-12-02T14:30:49Z |
|
6653268 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T01:44:23Z |
|
c683180 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T23:03:28Z |
|
b8939b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T11:15:19Z |
|
cf45637 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
15 |
2023-12-03T03:38:27Z |
|
b2473f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
10 |
2023-12-01T01:46:08Z |
|
2fbad06 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T15:07:47+01:00 |
63e7474 |
21e1f92 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T04:29:03+01:00 |
bae6b57 |
f280c00 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-17T06:04:40+01:00 |
6653268 |
4c1e072 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T11:35:59+01:00 |
ef2678b |
6791ee4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T01:32:46+01:00 |
fe8189e |
f83e935 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T18:33:09+01:00 |
1dd18bd |
2fecc40 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T09:54:31+01:00 |
29f958f |
0e3cdaa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T06:01:05+01:00 |
cf45637 |
b913b88 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-01T03:40:16+01:00 |
b2473f4 |
3611d84 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T12:41:18+01:00 |
80192a6 |
80192a6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T05:10:22+01:00 |
|
ce64398 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T02:29:46+01:00 |
c683180 |
192093a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T18:25:12+01:00 |
b8939b9 |
f67cb74 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T08:07:49+01:00 |
72d53ef |
fe8189e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-04T00:33:43+01:00 |
|
63e7474 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
7 |
2023-12-19T13:58:58+01:00 |
|
bae6b57 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-18T23:44:49+01:00 |
|
72d53ef |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
15 |
2023-11-29T01:55:37Z |
|
977bdf4 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-11-30T22:32:17Z |
|
52c47d0 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 74e0f6e6-d746-46ec-bf87-5e24dc501825
creation_time: '2023-12-02T15:30:49+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c40e31fe-ff67-4e50-afd0-0b0e77eef9ac/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c40e31fe-ff67-4e50-afd0-0b0e77eef9ac/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
: dab3cfcd7f834fcfbdfecec143b1f55491432e66d7189ec50c725339851d6e17
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content: [
] |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T12:03:19+01:00 |
|
84f44aa |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 245b658c-251a-463b-9743-21dcedf02a09
creation_time: '2023-12-03T04:38:27+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8d727ad5-68b1-4b3e-a074-9f8ab637af19/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8d727ad5-68b1-4b3e-a074-9f8ab637af19/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
: dab3cfcd7f834fcfbdfecec143b1f55491432e66d7189ec50c725339851d6e17
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content: [
] |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T05:31:48+01:00 |
|
41d59fa |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 1e914e28-c4ba-4e28-8f8a-20c24ff885f2
creation_time: '2023-11-29T02:55:37+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_05d1eb6c-f6d5-44b5-b5fe-111f8ab108b3/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_05d1eb6c-f6d5-44b5-b5fe-111f8ab108b3/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
: dab3cfcd7f834fcfbdfecec143b1f55491432e66d7189ec50c725339851d6e17
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content: [
] |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:47:45+01:00 |
|
60893b6 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 2fd207f3-4fc0-4fff-975f-a6af67319766
creation_time: 2023-12-01T01:46:08Z
producer:
name: Goblint
version: tags/svcomp24-0-gc2e9465a7
command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification''
''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture''
''64bit'' ''../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i'''
task:
input_files:
- ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
input_file_hashes:
../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i: dab3cfcd7f834fcfbdfecec143b1f55491432e66d7189ec50c725339851d6e17
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrpbrk-alloca-1.i
file_hash: dab3cfcd7f834fcfbdfecec143b1f55491432e66d7189ec50c725339851d6e17
line: 552
column: 9
function: cstrpbrk
value: ((c == 0 || ((((4294967296LL + (long long )c) + (long long )sc >= 0LL
&& (4294967295LL - (long long )c) + (long long )sc >= 0LL) && (4294967295LL
+ (long long )c) - (long long )sc >= 0LL) && (4294967294LL - (long long )c)
- (long long )sc >= 0LL)) || ((((4294967296LL + (long long )c) + (long long
)sc >= 0LL && (4294967295LL - (long long )c) + (long long )sc >= 0LL) && (4294967295LL
+ (long long )c) - (long long )sc >= 0LL) && (4294967294LL - (long long )c)
- (long long )sc >= 0LL)) || ((((4294967296LL + (long long )c) + (long long
)sc >= 0LL && (4294967295LL - (long long )c) + (long long )sc >= 0LL) && (4294967295LL
+ (long long )c) - (long long )sc >= 0LL) && (4294967294LL - (long long )c)
- (long long )sc >= 0LL)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-01T03:58:49+01:00 |
|