fe59110 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T10:41:18+01:00 |
|
4fe86eb |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:23:07Z |
|
9c0b659 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T08:03:17+01:00 |
|
ee521a4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T22:18:00+01:00 |
|
520ff52 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
10 |
2023-12-18T01:35:40+01:00 |
|
ec695e4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T12:35:07Z |
|
1886ebd |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T13:18:14Z |
|
54d7ab5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T21:06:39Z |
|
b651ee6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T13:58:28Z |
|
08bdd98 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-19T01:13:36+01:00 |
|
01b69bc |
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-02T14:13:32Z |
|
6e5d4e6 |
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:56Z |
|
dce0358 |
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:27:25Z |
|
217ce36 |
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 |
738 |
2023-12-17T17:32:07+01:00 |
|
ce08af3 |
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-29T06:10:30Z |
|
330b486 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
8 |
2023-12-17T21:50:50+01:00 |
4efda52 |
c0048af |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:40:30+01:00 |
|
aaedb50 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T06:40:50Z |
|
3e3f079 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
cf20f4d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
13 |
2023-12-02T12:32:20Z |
|
9e23193 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T04:04:21Z |
|
b9228fe |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:49:37Z |
|
ab2bc58 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T21:19:03 |
|
02a6e56 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T14:03:22Z |
|
57955c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 7.4.0 kind |
3 |
2023-12-01T16:57:17Z |
|
5a061ea |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-20T02:16:38+01:00 |
ab2bc58 |
10fa91f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-17T06:24:06+01:00 |
9e23193 |
e1c083f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-05T14:20:44+01:00 |
b1c3f30 |
4dea057 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T16:29:28+01:00 |
cbbe10c |
9bcbe44 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:30:35+01:00 |
cf20f4d |
b07b019 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:35:36+01:00 |
c0048af |
52d3242 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T09:54:01+01:00 |
aaedb50 |
32667f0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T22:47:08+01:00 |
5d55f59 |
35b66e0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T18:11:44+01:00 |
57955c4 |
f01acad |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T05:34:43+01:00 |
|
af4f7da |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T02:43:09+01:00 |
b9228fe |
8703ef2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T18:21:16+01:00 |
02a6e56 |
3a407c6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:56:06+01:00 |
3372908 |
56d86da |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-04T00:04:46+01:00 |
|
a441f14 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T17:47:44+01:00 |
|
4efda52 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CBMC |
725 |
2023-12-17T15:46:59+01:00 |
|
b1c3f30 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T10:31:07Z |
|
cbbe10c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T14:52:31Z |
|
5d55f59 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:50:58Z |
|
3372908 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
14 |
2023-11-29T03:00:39Z |
|
88b7de6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T14:18:57Z |
|
6c28908 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T21:43:40Z |
|
ba85deb |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T22:03:43 |
|
514d11a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
725 |
2023-12-17T08:59:11+01:00 |
|
1d11e6f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T08:56:56Z |
|
cd10ff6 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T09:45:16Z |
|
f12541e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T21:08:48Z |
|
ab3bd88 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: f927e826-4cd2-4f6a-97e5-ba55fc83f675
creation_time: '2023-11-29T04:00:39+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
line: 28
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_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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:49:01+01:00 |
|
a7a7506 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 4ad5c713-554c-4e45-a69b-e98bd1fbdfa9
creation_time: '2023-12-02T13:32:20+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
line: 28
column: 0
function: main
value: ((0 <= i) && (i <= 2147483645))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T12:03:29+01:00 |
|
e673554 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: d2312ea7-1808-4581-9c5e-b259eadc6e5f
creation_time: 2023-12-01T01:58:02Z
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/ArraysOfVariableLength4.c'''
task:
input_files:
- ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
input_file_hashes:
../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
line: 15
column: 8
function: foo
value: 32 == size
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
line: 15
column: 8
function: foo
value: size == 32
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
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/ArraysOfVariableLength4.c
file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
line: 28
column: 5
function: main
value: (((((((((((((((((((((((((((((((((((((((((((((((((((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) || 8 <= 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) || i == 8) || i
== 22) || i == 7) || i == 21
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
19 |
2023-12-01T04:45:12+01:00 |
|