5cce7cf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:01:47Z |
|
8b3436c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:49:08+01:00 |
|
7986203 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
8bc887d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
10 |
2023-12-02T15:46:00Z |
|
854515d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T14:58:50Z |
|
4f36629 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-20T03:41:16+01:00 |
7986203 |
d2598bf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-19T15:07:44+01:00 |
5e705fb |
ca9d439 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T04:17:27+01:00 |
b998cac |
3d919a5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-17T06:04:45+01:00 |
2c35163 |
47c051c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:24:36+01:00 |
8bc887d |
f5d30f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T01:47:04+01:00 |
ee4e933 |
0c9b74f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:31:14+01:00 |
8b3436c |
cc0e586 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T10:00:55+01:00 |
5cce7cf |
5310246 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T00:15:47+01:00 |
7b885b7 |
1c7d41f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T12:29:11+01:00 |
a1ad225 |
a1ad225 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T06:11:43+01:00 |
|
6c5857c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T18:35:20+01:00 |
854515d |
97081aa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:59:38+01:00 |
886f193 |
ee4e933 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T23:28:48+01:00 |
|
2c35163 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
8 |
2023-12-17T02:55:50+01:00 |
|
b998cac |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T18:42:24+01:00 |
|
886f193 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
10 |
2023-11-28T22:45:59Z |
|
7b885b7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
14 |
2023-11-30T23:02:17+01:00 |
|
eb7f5a6 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
11 |
2023-11-30T21:12:27+01:00 |
|
366ea32 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: b94272dd-edfb-4602-b418-34387618e666
creation_time: '2023-11-28T23:45:59+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96dcef46-9872-4156-b783-3d4c09a83b4f/sv-benchmarks/c/termination-crafted/Stockholm-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96dcef46-9872-4156-b783-3d4c09a83b4f/sv-benchmarks/c/termination-crafted/Stockholm-1.c
: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96dcef46-9872-4156-b783-3d4c09a83b4f/sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 0
function: main
value: ((((((((3 * b) + x) <= (268435452 + (3 * a))) && (0 <= (268435455 + a))) && (b <= (536870910 + a))) && ((a + x) <= 536870906)) && (a <= b)) || (((((a <= 268435455) && (0 <= (268435455 + a))) && (b <= (536870910 + a))) && (a <= b)) && (x <= 268435455)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-11-29T07:50:02+01:00 |
|
cf6e5ae |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 6d803b27-e84f-45e3-9aa5-ed1438536d59
creation_time: 2023-12-02T16:46+01:00
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e43b6a26-c88d-4442-b38b-514e8a6bfd6e/sv-benchmarks/c/termination-crafted/Stockholm-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e43b6a26-c88d-4442-b38b-514e8a6bfd6e/sv-benchmarks/c/termination-crafted/Stockholm-1.c
: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e43b6a26-c88d-4442-b38b-514e8a6bfd6e/sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 0
function: main
value: (((((a <= 268435455) && (a == b)) && (0 <= (268435455 + b))) && (x <= 268435455)) && (0 <= (268435455 + x)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T12:03:48+01:00 |
|
33cb9b4 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: da52e475-28bd-4b3b-a733-e6b26a1d01cb
creation_time: 2023-12-01T01:13:31Z
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-crafted/Stockholm-1.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted/Stockholm-1.c: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: -268435455 <= a
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: -268435455 <= b
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: a <= 268435455
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: b <= 268435455
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: (536870910LL + (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: (0LL - (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: (536870910LL - (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: (long long )a - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Stockholm-1.c
file_hash: 0690e5781abea147059c8c3687dc0be9b462edcdf26c7ee50864c7e6884a231b
line: 26
column: 15
function: main
value: ((((((((-536870911 <= x && (268435456LL + (long long )a) + (long long
)x >= 0LL) && (268435456LL + (long long )b) + (long long )x >= 0LL) && (268435456LL
- (long long )a) + (long long )x >= 0LL) && (268435456LL - (long long )b)
+ (long long )x >= 0LL) && (((((((((((((((x <= 2147483646 && (((((((((((4294967265LL
+ (long long )a) - (long long )x >= 0LL && (4294967265LL + (long long )b)
- (long long )x >= 0LL) && (4294967265LL - (long long )a) - (long long )x
>= 0LL) && (4294967265LL - (long long )b) - (long long )x >= 0LL) || ((((4026531811LL
+ (long long )a) - (long long )x >= 0LL && (4026531811LL + (long long )b)
- (long long )x >= 0LL) && (4026531811LL - (long long )a) - (long long )x
>= 0LL) && (4026531811LL - (long long )b) - (long long )x >= 0LL)) || ((((3758096357LL
+ (long long )a) - (long long )x >= 0LL && (3758096357LL + (long long )b)
- (long long )x >= 0LL) && (3758096357LL - (long long )a) - (long long )x
>= 0LL) && (3758096357LL - (long long )b) - (long long )x >= 0LL)) || ((((3489660903LL
+ (long long )a) - (long long )x >= 0LL && (3489660903LL + (long long )b)
- (long long )x >= 0LL) && (3489660903LL - (long long )a) - (long long )x
>= 0LL) && (3489660903LL - (long long )b) - (long long )x >= 0LL)) || ((((3221225449LL
+ (long long )a) - (long long )x >= 0LL && (3221225449LL + (long long )b)
- (long long )x >= 0LL) && (3221225449LL - (long long )a) - (long long )x
>= 0LL) && (3221225449LL - (long long )b) - (long long )x >= 0LL)) || ((((2952789995LL
+ (long long )a) - (long long )x >= 0LL && (2952789995LL + (long long )b)
- (long long )x >= 0LL) && (2952789995LL - (long long )a) - (long long )x
>= 0LL) && (2952789995LL - (long long )b) - (long long )x >= 0LL)) || ((((2684354541LL
+ (long long )a) - (long long )x >= 0LL && (2684354541LL + (long long )b)
- (long long )x >= 0LL) && (2684354541LL - (long long )a) - (long long )x
>= 0LL) && (2684354541LL - (long long )b) - (long long )x >= 0LL)) || ((((2415919087LL
+ (long long )a) - (long long )x >= 0LL && (2415919087LL + (long long )b)
- (long long )x >= 0LL) && (2415919087LL - (long long )a) - (long long )x
>= 0LL) && (2415919087LL - (long long )b) - (long long )x >= 0LL))) || ((((x
<= 2147483633 && (2147483633LL + (long long )a) - (long long )x >= 0LL) &&
(2147483633LL + (long long )b) - (long long )x >= 0LL) && (2147483633LL -
(long long )a) - (long long )x >= 0LL) && (2147483633LL - (long long )b) -
(long long )x >= 0LL)) || x <= 2147483646) || ((((x <= 1879048179 && (1879048179LL
+ (long long )a) - (long long )x >= 0LL) && (1879048179LL + (long long )b)
- (long long )x >= 0LL) && (1879048179LL - (long long )a) - (long long )x
>= 0LL) && (1879048179LL - (long long )b) - (long long )x >= 0LL)) || ((((x
<= 2147483646 && (6710886351LL + (long long )a) - (long long )x >= 0LL) &&
(6710886351LL + (long long )b) - (long long )x >= 0LL) && (6710886351LL -
(long long )a) - (long long )x >= 0LL) && (6710886351LL - (long long )b) -
(long long )x >= 0LL)) || ((((x <= 1610612725 && (1610612725LL + (long long
)a) - (long long )x >= 0LL) && (1610612725LL + (long long )b) - (long long
)x >= 0LL) && (1610612725LL - (long long )a) - (long long )x >= 0LL) && (1610612725LL
- (long long )b) - (long long )x >= 0LL)) || ((((x <= 2147483646 && (6442450897LL
+ (long long )a) - (long long )x >= 0LL) && (6442450897LL + (long long )b)
- (long long )x >= 0LL) && (6442450897LL - (long long )a) - (long long )x
>= 0LL) && (6442450897LL - (long long )b) - (long long )x >= 0LL)) || ((((x
<= 1342177271 && (1342177271LL + (long long )a) - (long long )x >= 0LL) &&
(1342177271LL + (long long )b) - (long long )x >= 0LL) && (1342177271LL -
(long long )a) - (long long )x >= 0LL) && (1342177271LL - (long long )b) -
(long long )x >= 0LL)) || ((((x <= 2147483646 && (6174015443LL + (long long
)a) - (long long )x >= 0LL) && (6174015443LL + (long long )b) - (long long
)x >= 0LL) && (6174015443LL - (long long )a) - (long long )x >= 0LL) && (6174015443LL
- (long long )b) - (long long )x >= 0LL)) || ((((x <= 1073741817 && (1073741817LL
+ (long long )a) - (long long )x >= 0LL) && (1073741817LL + (long long )b)
- (long long )x >= 0LL) && (1073741817LL - (long long )a) - (long long )x
>= 0LL) && (1073741817LL - (long long )b) - (long long )x >= 0LL)) || ((((x
<= 2147483646 && (5905579989LL + (long long )a) - (long long )x >= 0LL) &&
(5905579989LL + (long long )b) - (long long )x >= 0LL) && (5905579989LL -
(long long )a) - (long long )x >= 0LL) && (5905579989LL - (long long )b) -
(long long )x >= 0LL)) || ((((x <= 805306363 && (805306363LL + (long long
)a) - (long long )x >= 0LL) && (805306363LL + (long long )b) - (long long
)x >= 0LL) && (805306363LL - (long long )a) - (long long )x >= 0LL) && (805306363LL
- (long long )b) - (long long )x >= 0LL)) || ((((x <= 2147483646 && (5637144535LL
+ (long long )a) - (long long )x >= 0LL) && (5637144535LL + (long long )b)
- (long long )x >= 0LL) && (5637144535LL - (long long )a) - (long long )x
>= 0LL) && (5637144535LL - (long long )b) - (long long )x >= 0LL)) || ((((x
<= 805306364 && (536870909LL + (long long )a) - (long long )x >= 0LL) && (536870909LL
+ (long long )b) - (long long )x >= 0LL) && (536870909LL - (long long )a)
- (long long )x >= 0LL) && (536870909LL - (long long )b) - (long long )x >=
0LL)) || ((((x <= 2147483646 && (5368709081LL + (long long )a) - (long long
)x >= 0LL) && (5368709081LL + (long long )b) - (long long )x >= 0LL) && (5368709081LL
- (long long )a) - (long long )x >= 0LL) && (5368709081LL - (long long )b)
- (long long )x >= 0LL))) || (((((((((-268435455 <= x && x <= 268435455) &&
(536870910LL + (long long )a) + (long long )x >= 0LL) && (536870910LL + (long
long )b) + (long long )x >= 0LL) && (536870910LL - (long long )a) + (long
long )x >= 0LL) && (536870910LL - (long long )b) + (long long )x >= 0LL) &&
(536870910LL + (long long )a) - (long long )x >= 0LL) && (536870910LL + (long
long )b) - (long long )x >= 0LL) && (536870910LL - (long long )a) - (long
long )x >= 0LL) && (536870910LL - (long long )b) - (long long )x >= 0LL))
|| (((((((((-536870911 <= x && x <= 2147483646) && (268435456LL + (long long
)a) + (long long )x >= 0LL) && (268435456LL + (long long )b) + (long long
)x >= 0LL) && (268435456LL - (long long )a) + (long long )x >= 0LL) && (268435456LL
- (long long )b) + (long long )x >= 0LL) && (5100273627LL + (long long )a)
- (long long )x >= 0LL) && (5100273627LL + (long long )b) - (long long )x
>= 0LL) && (5100273627LL - (long long )a) - (long long )x >= 0LL) && (5100273627LL
- (long long )b) - (long long )x >= 0LL)) || (((((((((-536870911 <= x && x
<= 2147483646) && (268435456LL + (long long )a) + (long long )x >= 0LL) &&
(268435456LL + (long long )b) + (long long )x >= 0LL) && (268435456LL - (long
long )a) + (long long )x >= 0LL) && (268435456LL - (long long )b) + (long
long )x >= 0LL) && (4831838173LL + (long long )a) - (long long )x >= 0LL)
&& (4831838173LL + (long long )b) - (long long )x >= 0LL) && (4831838173LL
- (long long )a) - (long long )x >= 0LL) && (4831838173LL - (long long )b)
- (long long )x >= 0LL)) || (((((((((-536870911 <= x && x <= 2147483646) &&
(268435456LL + (long long )a) + (long long )x >= 0LL) && (268435456LL + (long
long )b) + (long long )x >= 0LL) && (268435456LL - (long long )a) + (long
long )x >= 0LL) && (268435456LL - (long long )b) + (long long )x >= 0LL) &&
(4563402719LL + (long long )a) - (long long )x >= 0LL) && (4563402719LL +
(long long )b) - (long long )x >= 0LL) && (4563402719LL - (long long )a) -
(long long )x >= 0LL) && (4563402719LL - (long long )b) - (long long )x >=
0LL)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
21 |
2023-12-01T04:32:58+01:00 |
|