4d51509 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T08:59:54+01:00 |
|
c6ea5c3 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T20:09:15Z |
|
5a9834f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T05:38:15+01:00 |
|
1b022eb |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T22:54:27+01:00 |
|
dd82193 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
11 |
2023-12-18T01:34:38+01:00 |
|
8ad89b1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T07:29:07Z |
|
7cf027d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T12:38:14Z |
|
fff2d1b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:35:45Z |
|
d93fc63 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T12:12:06Z |
|
dc948b4 |
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:42:46Z |
|
17204e7 |
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:16Z |
|
29df739 |
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-29T15:45:58Z |
|
387fa42 |
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 |
748 |
2023-12-17T15:38:13+01:00 |
|
4417545 |
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-29T00:12:21Z |
|
cde06ff |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-19T00:23:33+01:00 |
|
bea556f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
8 |
2023-12-17T21:51:48+01:00 |
abe6070 |
8bf4ca9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:45:25+01:00 |
|
fbc4065 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:44:28Z |
|
ef92c9c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
b9bc9a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
14 |
2023-12-02T12:36:59Z |
|
4d2c37f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T00:50:13Z |
|
23529c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T21:39:44Z |
|
43f1aa4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T22:27:30 |
|
76bbb7c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T14:34:17Z |
|
3ed177e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 7.4.0 kind |
3 |
2023-12-01T14:10:39Z |
|
beff01c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-20T02:18:28+01:00 |
43f1aa4 |
4d1b0cc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-17T06:09:02+01:00 |
4d2c37f |
ec52713 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-05T14:23:09+01:00 |
e7b1099 |
3b3ea66 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T16:29:46+01:00 |
f360ad0 |
516cb4e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:24:11+01:00 |
b9bc9a7 |
e75a051 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:32:32+01:00 |
8bf4ca9 |
b2fc5b7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T09:54:44+01:00 |
fbc4065 |
7c06f89 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T22:44:59+01:00 |
16af9f4 |
85c36d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T18:16:48+01:00 |
3ed177e |
9a428c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T08:50:08+01:00 |
|
9776a2d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T02:31:38+01:00 |
23529c8 |
6c80ff2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T18:11:30+01:00 |
76bbb7c |
be91ce6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T08:12:08+01:00 |
3425181 |
91bfd43 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T21:38:10+01:00 |
|
293347f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T22:08:28+01:00 |
|
abe6070 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CBMC |
735 |
2023-12-17T17:57:30+01:00 |
|
e7b1099 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T09:24:02Z |
|
f360ad0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T13:39:33Z |
|
16af9f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:55:59Z |
|
3425181 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
14 |
2023-11-29T06:09:12Z |
|
d032114 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T13:27:18Z |
|
33c0a88 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:57:16Z |
|
d871cd8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T21:52:16 |
|
d1c196b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
735 |
2023-12-17T18:37:05+01:00 |
|
2eb563f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T10:00:06Z |
|
700e11b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T13:34:23Z |
|
7717221 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:45:17Z |
|
056f7fc |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: b0c8dbc8-45f7-45e1-9dde-98f29a344a34
creation_time: '2023-12-02T13:36:59+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
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_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 25
column: 0
function: main
value: ((0 <= i) && (i <= 2147483647))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 29
column: 0
function: main
value: ((0 <= i) && (i <= 2147483647))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T11:58:11+01:00 |
|
0c7a954 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 752537b5-bd54-4980-a726-bb7582621bd5
creation_time: '2023-11-29T07:09:12+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
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_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 25
column: 0
function: main
value: ((i <= 2147483646) && (0 <= (i + 2147483648)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 29
column: 0
function: main
value: ((i <= 2147483644) && (0 <= (i + 2147483648)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 15
column: 0
function: foo
value: (((((((i % 4294967296) <= 31) && (32 == size)) && (0 <= (i + 2147483648))) && (i == 0)) && (i <= 2147483645)) || ((((((i % 4294967296) <= 31) && (0 <= (i + 2147483648))) && (size <= 32)) && (1 <= i)) && (i <= 2147483645)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
10 |
2023-11-29T07:45:43+01:00 |
|
bd9d4af |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 0388eae5-3a21-4153-b461-5b74cd36526a
creation_time: 2023-12-01T01:28:50Z
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/ArraysOfVariableLength6.c'''
task:
input_files:
- ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
input_file_hashes:
../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
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/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 15
column: 8
function: foo
value: 32 == size
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 15
column: 8
function: foo
value: size == 32
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 15
column: 8
function: foo
value: (((((((((((((((((((((((((((12 <= i && (-44LL + (long long )i) + (long
long )size >= 0LL) && (20LL + (long long )i) - (long long )size >= 0LL) &&
(((i <= 31 && (-1LL - (long long )i) + (long long )size >= 0LL) && (63LL -
(long long )i) - (long long )size >= 0LL) || ((i <= 32 && (0LL - (long long
)i) + (long long )size >= 0LL) && (64LL - (long long )i) - (long long )size
>= 0LL))) || (((((-43LL + (long long )i) + (long long )size >= 0LL && (-21LL
- (long long )i) + (long long )size >= 0LL) && (21LL + (long long )i) - (long
long )size >= 0LL) && (43LL - (long long )i) - (long long )size >= 0LL) &&
i == 11)) || (((((-43LL + (long long )i) + (long long )size >= 0LL && (-21LL
- (long long )i) + (long long )size >= 0LL) && (21LL + (long long )i) - (long
long )size >= 0LL) && (43LL - (long long )i) - (long long )size >= 0LL) &&
i == 11)) || (((((-42LL + (long long )i) + (long long )size >= 0LL && (-22LL
- (long long )i) + (long long )size >= 0LL) && (22LL + (long long )i) - (long
long )size >= 0LL) && (42LL - (long long )i) - (long long )size >= 0LL) &&
i == 10)) || (((((-42LL + (long long )i) + (long long )size >= 0LL && (-22LL
- (long long )i) + (long long )size >= 0LL) && (22LL + (long long )i) - (long
long )size >= 0LL) && (42LL - (long long )i) - (long long )size >= 0LL) &&
i == 10)) || (((((-41LL + (long long )i) + (long long )size >= 0LL && (-23LL
- (long long )i) + (long long )size >= 0LL) && (23LL + (long long )i) - (long
long )size >= 0LL) && (41LL - (long long )i) - (long long )size >= 0LL) &&
i == 9)) || (((((-41LL + (long long )i) + (long long )size >= 0LL && (-23LL
- (long long )i) + (long long )size >= 0LL) && (23LL + (long long )i) - (long
long )size >= 0LL) && (41LL - (long long )i) - (long long )size >= 0LL) &&
i == 9)) || (((((-40LL + (long long )i) + (long long )size >= 0LL && (-24LL
- (long long )i) + (long long )size >= 0LL) && (24LL + (long long )i) - (long
long )size >= 0LL) && (40LL - (long long )i) - (long long )size >= 0LL) &&
i == 8)) || (((((-40LL + (long long )i) + (long long )size >= 0LL && (-24LL
- (long long )i) + (long long )size >= 0LL) && (24LL + (long long )i) - (long
long )size >= 0LL) && (40LL - (long long )i) - (long long )size >= 0LL) &&
i == 8)) || (((((-39LL + (long long )i) + (long long )size >= 0LL && (-25LL
- (long long )i) + (long long )size >= 0LL) && (25LL + (long long )i) - (long
long )size >= 0LL) && (39LL - (long long )i) - (long long )size >= 0LL) &&
i == 7)) || (((((-39LL + (long long )i) + (long long )size >= 0LL && (-25LL
- (long long )i) + (long long )size >= 0LL) && (25LL + (long long )i) - (long
long )size >= 0LL) && (39LL - (long long )i) - (long long )size >= 0LL) &&
i == 7)) || (((((-38LL + (long long )i) + (long long )size >= 0LL && (-26LL
- (long long )i) + (long long )size >= 0LL) && (26LL + (long long )i) - (long
long )size >= 0LL) && (38LL - (long long )i) - (long long )size >= 0LL) &&
i == 6)) || (((((-38LL + (long long )i) + (long long )size >= 0LL && (-26LL
- (long long )i) + (long long )size >= 0LL) && (26LL + (long long )i) - (long
long )size >= 0LL) && (38LL - (long long )i) - (long long )size >= 0LL) &&
i == 6)) || (((((-37LL + (long long )i) + (long long )size >= 0LL && (-27LL
- (long long )i) + (long long )size >= 0LL) && (27LL + (long long )i) - (long
long )size >= 0LL) && (37LL - (long long )i) - (long long )size >= 0LL) &&
i == 5)) || (((((-37LL + (long long )i) + (long long )size >= 0LL && (-27LL
- (long long )i) + (long long )size >= 0LL) && (27LL + (long long )i) - (long
long )size >= 0LL) && (37LL - (long long )i) - (long long )size >= 0LL) &&
i == 5)) || (((((-36LL + (long long )i) + (long long )size >= 0LL && (-28LL
- (long long )i) + (long long )size >= 0LL) && (28LL + (long long )i) - (long
long )size >= 0LL) && (36LL - (long long )i) - (long long )size >= 0LL) &&
i == 4)) || (((((-36LL + (long long )i) + (long long )size >= 0LL && (-28LL
- (long long )i) + (long long )size >= 0LL) && (28LL + (long long )i) - (long
long )size >= 0LL) && (36LL - (long long )i) - (long long )size >= 0LL) &&
i == 4)) || (((((-35LL + (long long )i) + (long long )size >= 0LL && (-29LL
- (long long )i) + (long long )size >= 0LL) && (29LL + (long long )i) - (long
long )size >= 0LL) && (35LL - (long long )i) - (long long )size >= 0LL) &&
i == 3)) || (((((-35LL + (long long )i) + (long long )size >= 0LL && (-29LL
- (long long )i) + (long long )size >= 0LL) && (29LL + (long long )i) - (long
long )size >= 0LL) && (35LL - (long long )i) - (long long )size >= 0LL) &&
i == 3)) || (((((-34LL + (long long )i) + (long long )size >= 0LL && (-30LL
- (long long )i) + (long long )size >= 0LL) && (30LL + (long long )i) - (long
long )size >= 0LL) && (34LL - (long long )i) - (long long )size >= 0LL) &&
i == 2)) || (((((-34LL + (long long )i) + (long long )size >= 0LL && (-30LL
- (long long )i) + (long long )size >= 0LL) && (30LL + (long long )i) - (long
long )size >= 0LL) && (34LL - (long long )i) - (long long )size >= 0LL) &&
i == 2)) || (((((-33LL + (long long )i) + (long long )size >= 0LL && (-31LL
- (long long )i) + (long long )size >= 0LL) && (31LL + (long long )i) - (long
long )size >= 0LL) && (33LL - (long long )i) - (long long )size >= 0LL) &&
i == 1)) || (((((-33LL + (long long )i) + (long long )size >= 0LL && (-31LL
- (long long )i) + (long long )size >= 0LL) && (31LL + (long long )i) - (long
long )size >= 0LL) && (33LL - (long long )i) - (long long )size >= 0LL) &&
i == 1)) || ((((((-32LL + (long long )i) + (long long )size >= 0LL && (-32LL
- (long long )i) + (long long )size >= 0LL) && (32LL + (long long )i) - (long
long )size >= 0LL) && (32LL - (long long )i) - (long long )size >= 0LL) &&
0 == i) && i == 0)) || ((((((-32LL + (long long )i) + (long long )size >=
0LL && (-32LL - (long long )i) + (long long )size >= 0LL) && (32LL + (long
long )i) - (long long )size >= 0LL) && (32LL - (long long )i) - (long long
)size >= 0LL) && 0 == i) && i == 0)) || ((((2147483616LL + (long long )i)
+ (long long )size >= 0LL && (2147483615LL - (long long )i) + (long long )size
>= 0LL) && (2147483680LL + (long long )i) - (long long )size >= 0LL) && (2147483679LL
- (long long )i) - (long long )size >= 0LL)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
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/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
line: 29
column: 5
function: main
value: c == mask
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c
file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
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 == 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 |
correctness_witness |
CPAchecker 2.3 |
19 |
2023-12-01T04:18:47+01:00 |
|