5b9c2df |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T08:48:07+01:00 |
|
0745c3a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T01:06:34Z |
|
4ca6db1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T23:50:28Z |
|
e00eebe |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T06:30:27+01:00 |
|
e7b1307 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T22:54:52+01:00 |
|
27723c0 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-19T00:57:19+01:00 |
|
8d482a5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
11 |
2023-12-18T01:56:31+01:00 |
|
408e98f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T12:37:34Z |
|
fdb953d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T08:51:23Z |
|
f28c72e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:57:07Z |
|
0139c23 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T03:31:27Z |
|
0ef34ab |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Taipan |
13 |
2023-12-02T11:36:20Z |
|
93f3e89 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
PredatorHP |
4 |
2023-11-30T08:24:02Z |
|
28b316b |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T09:03:20Z |
|
86dc981 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
397 |
2023-12-17T19:55:29+01:00 |
|
dee016c |
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 |
13 |
2023-11-29T02:36:07Z |
|
710c019 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-17T21:37:04+01:00 |
72cb163 |
9f1deb6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
63 |
2023-12-04T11:41:56+01:00 |
835255b |
eccf67a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
17 |
2023-11-29T08:01:47+01:00 |
a62e936 |
28c0a0c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:16:43+01:00 |
|
e3ebdd5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:15:33Z |
|
ec930ee |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
835255b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
14 |
2023-12-02T16:19:32Z |
|
b4cc155 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T00:41:08Z |
|
25e5270 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:12:38Z |
|
45c1662 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T21:05:25 |
|
3615534 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T06:23:00Z |
|
121c719 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 7.4.0 kind |
3 |
2023-12-01T11:00:51Z |
|
57af88d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-20T02:17:54+01:00 |
45c1662 |
ee54d87 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-17T06:27:06+01:00 |
b4cc155 |
9a06456 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-05T14:21:29+01:00 |
03c096c |
b103f37 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T16:28:22+01:00 |
24f1def |
8a0072d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:29:42+01:00 |
28c0a0c |
6b00ab7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T09:54:56+01:00 |
e3ebdd5 |
a7c8f43 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T22:46:03+01:00 |
6442cc1 |
7c7897e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T17:37:03+01:00 |
121c719 |
e47b283 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T05:42:24+01:00 |
|
948e584 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T02:27:57+01:00 |
25e5270 |
5ebddc8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T18:14:58+01:00 |
3615534 |
2ad45df |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T22:23:25+01:00 |
|
20207d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T23:08:17+01:00 |
|
72cb163 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CBMC |
396 |
2023-12-17T13:11:04+01:00 |
|
03c096c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T11:01:35Z |
|
24f1def |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T12:50:18Z |
|
6442cc1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T21:10:09Z |
|
a62e936 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
14 |
2023-11-29T01:11:29Z |
|
a2c1760 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: e06c4ac7-c6ff-4875-83d3-90d7beae6591
creation_time: '2023-12-02T17:19:32+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d59cf96a-7f9b-4fd2-8fdd-7ad5344975bf/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d59cf96a-7f9b-4fd2-8fdd-7ad5344975bf/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 32bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d59cf96a-7f9b-4fd2-8fdd-7ad5344975bf/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 25
column: 0
function: main
value: ((i == 0) || ((i <= 2147483646) && (1 <= i)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d59cf96a-7f9b-4fd2-8fdd-7ad5344975bf/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 29
column: 0
function: main
value: ((i == 0) || ((i <= 2147483646) && (1 <= i)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T11:56:45+01:00 |
|
47a31ac |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 0690f56b-7618-4fc3-87ee-a34ff80f193d
creation_time: '2023-11-29T02:11:29+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f8cf72d-2400-4069-824d-bfc70b6ef92e/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f8cf72d-2400-4069-824d-bfc70b6ef92e/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 32bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f8cf72d-2400-4069-824d-bfc70b6ef92e/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 25
column: 0
function: main
value: ((i == 0) || ((i <= 2147483646) && (1 <= i)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f8cf72d-2400-4069-824d-bfc70b6ef92e/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 29
column: 0
function: main
value: ((i == 0) || ((i <= 2147483646) && (1 <= i)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f8cf72d-2400-4069-824d-bfc70b6ef92e/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 15
column: 0
function: foo
value: (((((i == 0) && (size == 0)) && (i == 0)) || ((((1 <= i) && (1 <= i)) && (i == size)) && (i <= 2147483645))) || ((((i == 0) && (1 <= size)) && (i == size)) && (i <= 2147483645)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
10 |
2023-11-29T07:51:18+01:00 |
|
1011370 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: e0aab5e5-1505-44bf-af64-c391b7e0a6d8
creation_time: 2023-12-01T01:02:26Z
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''
''32bit'' ''../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c'''
task:
input_files:
- ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
input_file_hashes:
../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
data_model: ILP32
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 29
column: 5
function: main
value: c == & mask[0]
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 29
column: 5
function: main
value: c == mask
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 29
column: 5
function: main
value: (((((((((((((((((((((((((((((((((((((((((((((((((((i == 8 || i == 22)
|| i == 7) || i == 21) || i == 7) || i == 21) || i == 6) || i == 20) || i
== 6) || i == 20) || i == 5) || i == 19) || i == 5) || i == 19) || i == 4)
|| i == 18) || i == 4) || i == 18) || i == 3) || i == 17) || i == 3) || i
== 17) || i == 2) || i == 16) || i == 2) || i == 16) || i == 1) || i == 15)
|| i == 1) || i == 15) || (0 == i && i == 0)) || i == 14) || (0 == i && i
== 0)) || i == 14) || 6 <= i) || i == 13) || i == 13) || i == 12) || i ==
12) || i == 11) || (25 <= i && i != 0)) || i == 11) || (25 <= i && i != 1))
|| i == 10) || i == 24) || i == 10) || i == 24) || i == 9) || i == 23) ||
i == 9) || i == 23) || i == 8) || i == 22
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength5.c
file_hash: c60dc3ce59c2c65912da9b7b458247bdc42b4524b29b39bec7ce63758c18c031
line: 15
column: 8
function: foo
value: ((size != 0 && ((((((((((((((((((((((((12 <= i && (((((13 <= size &&
i <= 2147483646) && (-25LL + (long long )i) + (long long )size >= 0LL) &&
(-1LL - (long long )i) + (long long )size >= 0LL) && i != 0) || ((12 <= size
&& (-24LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long
)i) + (long long )size >= 0LL))) || (((12 <= size && (-23LL + (long long )i)
+ (long long )size >= 0LL) && (-1LL - (long long )i) + (long long )size >=
0LL) && i == 11)) || (((11 <= size && (-22LL + (long long )i) + (long long
)size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i ==
11)) || (((11 <= size && (-21LL + (long long )i) + (long long )size >= 0LL)
&& (-1LL - (long long )i) + (long long )size >= 0LL) && i == 10)) || (((10
<= size && (-20LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long
long )i) + (long long )size >= 0LL) && i == 10)) || (((10 <= size && (-19LL
+ (long long )i) + (long long )size >= 0LL) && (-1LL - (long long )i) + (long
long )size >= 0LL) && i == 9)) || (((9 <= size && (-18LL + (long long )i)
+ (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >=
0LL) && i == 9)) || (((9 <= size && (-17LL + (long long )i) + (long long )size
>= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && i == 8)) ||
(((8 <= size && (-16LL + (long long )i) + (long long )size >= 0LL) && (0LL
- (long long )i) + (long long )size >= 0LL) && i == 8)) || (((8 <= size &&
(-15LL + (long long )i) + (long long )size >= 0LL) && (-1LL - (long long )i)
+ (long long )size >= 0LL) && i == 7)) || (((7 <= size && (-14LL + (long long
)i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size
>= 0LL) && i == 7)) || (((7 <= size && (-13LL + (long long )i) + (long long
)size >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && i ==
6)) || (((6 <= size && (-12LL + (long long )i) + (long long )size >= 0LL)
&& (0LL - (long long )i) + (long long )size >= 0LL) && i == 6)) || (((6 <=
size && (-11LL + (long long )i) + (long long )size >= 0LL) && (-1LL - (long
long )i) + (long long )size >= 0LL) && i == 5)) || (((5 <= size && (-10LL
+ (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long
long )size >= 0LL) && i == 5)) || (((5 <= size && (-9LL + (long long )i) +
(long long )size >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL)
&& i == 4)) || (((4 <= size && (-8LL + (long long )i) + (long long )size >=
0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 4)) || (((4
<= size && (-7LL + (long long )i) + (long long )size >= 0LL) && (-1LL - (long
long )i) + (long long )size >= 0LL) && i == 3)) || (((3 <= size && (-6LL +
(long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long
long )size >= 0LL) && i == 3)) || (((3 <= size && (-5LL + (long long )i) +
(long long )size >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL)
&& i == 2)) || (((2 <= size && (-4LL + (long long )i) + (long long )size >=
0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 2)) || (((2
<= size && (-3LL + (long long )i) + (long long )size >= 0LL) && (-1LL - (long
long )i) + (long long )size >= 0LL) && i == 1)) || (((1 <= size && (-2LL +
(long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long
long )size >= 0LL) && i == 1)) || ((((1 <= size && (-1LL + (long long )i)
+ (long long )size >= 0LL) && (-1LL - (long long )i) + (long long )size >=
0LL) && 0 == i) && i == 0))) || (((0 <= size && (0LL - (long long )i) + (long
long )size >= 0LL) && (long long )i + (long long )size >= 0LL) && i == 0))
|| ((0 <= size && (2147483648LL + (long long )i) + (long long )size >= 0LL)
&& (2147483647LL - (long long )i) + (long long )size >= 0LL)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
16 |
2023-12-01T04:25:09+01:00 |
|