2e68107 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:58:44Z |
|
f09cde2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:57:15+01:00 |
|
f8918ef |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
34fb784 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
9 |
2023-12-02T16:20:01Z |
|
848a796 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-20T03:41:52+01:00 |
f8918ef |
ac1ad00 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-19T14:41:56+01:00 |
da8b62a |
d928673 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-19T03:41:06+01:00 |
3b223fb |
0e87fad |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-17T06:26:27+01:00 |
880d32b |
27e32c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-04T11:35:21+01:00 |
34fb784 |
e4d5d45 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-04T01:34:47+01:00 |
865c84c |
3e7065f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-03T18:31:03+01:00 |
f09cde2 |
f3f2e9d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-03T09:57:53+01:00 |
2e68107 |
a1806db |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T12:13:16+01:00 |
1d1cd65 |
1d1cd65 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T04:38:43+01:00 |
|
9e13ea1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-29T08:19:52+01:00 |
bf7fe40 |
865c84c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
4 |
2023-12-03T21:37:51+01:00 |
|
880d32b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
4 |
2023-12-17T05:19:35+01:00 |
|
da8b62a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
4 |
2023-12-19T10:36:47+01:00 |
|
3b223fb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2023-12-18T18:14:02+01:00 |
|
bf7fe40 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
8 |
2023-11-29T00:58:41Z |
|
23be7cd |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T01:47:47Z |
|
1506b2d |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: c0b162e3-a837-43b1-9e38-22d254990ea5
creation_time: '2023-11-29T01:58:41+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f163e3af-54ac-498f-bae2-74a31c1b8635/sv-benchmarks/c/termination-crafted/Benghazi.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f163e3af-54ac-498f-bae2-74a31c1b8635/sv-benchmarks/c/termination-crafted/Benghazi.c
: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
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_f163e3af-54ac-498f-bae2-74a31c1b8635/sv-benchmarks/c/termination-crafted/Benghazi.c
file_hash: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
line: 22
column: 0
function: main
value: (((((d2 == 74) && (x <= 2147483647)) && (d1 == 73)) || (((((d2 == 74) && (d1 == 75)) && (0 <= (x + 73))) && (d1 == 73)) && (x <= 2147483574))) || (((((((((((((73 <= d1) && (d2 <= 2147483647)) && (75 <= d1)) && (d1 <= 2147483645)) && (d1 <= 2147483645)) && (((d1 * 4) + (3 * x)) <= 8589934572)) && ((x + d1) <= 2147483647)) && (0 <= (x + d1))) && (x <= 2147483499)) && (1 <= (d2 + x))) && (((d2 * 4) + (3 * x)) <= 8589934576)) && (74 <= d2)) && ((d2 + x) <= 2147483648)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T07:48:52+01:00 |
|
fa13793 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 5f53449b-f352-41ff-a51b-54bfa00bd549
creation_time: '2023-12-02T17:20:01+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c875c161-2fd4-4012-beed-5cacfd62de71/sv-benchmarks/c/termination-crafted/Benghazi.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c875c161-2fd4-4012-beed-5cacfd62de71/sv-benchmarks/c/termination-crafted/Benghazi.c
: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
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_c875c161-2fd4-4012-beed-5cacfd62de71/sv-benchmarks/c/termination-crafted/Benghazi.c
file_hash: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
line: 22
column: 0
function: main
value: (((((((((d2 == 74) && (d1 == 75)) && (0 <= (x + 73))) && (d1 == 73)) && (x <= 2147483574)) || ((((d2 == 74) && (x <= 2147483647)) && (0 <= (x + 2147483648))) && (d1 == 73))) || (((((76 == d2) && (d1 == 75)) && (0 <= (x + 75))) && (d1 == 75)) && (x <= 2147483499))) || ((((((d1 <= 2147483645) && (d1 <= 2147483645)) && ((((((d1 + x) <= 2147483570) && (75 <= d1)) && ((d1 + 1) == d2)) && (77 <= d1)) || (((((d1 + 1) == d2) && ((x + (2 * d1)) <= 2147483570)) && (79 <= d1)) && (74 <= d2)))) && (1 <= (d2 + x))) && (((d2 * 4) + (3 * x)) <= 8589934576)) && ((d2 + x) <= 2147483648))) || (((((((d2 + x) <= 2147483500) && (77 == d1)) && ((d1 + 1) == d2)) && (d2 <= 76)) && (1 <= (d2 + x))) && (74 <= d2)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T12:04:53+01:00 |
|
9eb6709 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 8295e511-5265-4e48-9e84-439e6e42371e
creation_time: 2023-12-01T01:52:55Z
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/Benghazi.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted/Benghazi.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted/Benghazi.c: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
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/Benghazi.c
file_hash: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
line: 22
column: 8
function: main
value: (((((-1LL + (long long )d2) + (long long )x >= 0LL && (-1LL - (long long
)d1old) + (long long )d2 >= 0LL) && (long long )d1old + (long long )x >= 0LL)
&& (1LL + (long long )d1old) - (long long )d2 >= 0LL) && (((((((1LL - (long
long )d1) + (long long )d2 >= 0LL && (2LL - (long long )d1) + (long long )d1old
>= 0LL) && ((((((((((((((-2147483647 <= x && 79 <= d1) && 79 <= d1old) &&
80 <= d2) && x <= 2147483191) && (-159LL + (long long )d1) + (long long )d2
>= 0LL) && (-159LL + (long long )d1old) + (long long )d2 >= 0LL) && (-158LL
+ (long long )d1) + (long long )d1old >= 0LL) && (long long )d1 + (long long
)x >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL) && (long long
)d1 - (long long )d1old >= 0LL) && d1 % 2 == 1) && d2 % 2 == 0) && d1old %
2 == 1) || ((((((((((((((((-77 <= x && x <= 2147483270) && (-157LL + (long
long )d1) + (long long )d2 >= 0LL) && (-156LL + (long long )d1) + (long long
)d1old >= 0LL) && (-155LL + (long long )d1old) + (long long )d2 >= 0LL) &&
(-2LL + (long long )d1) + (long long )x >= 0LL) && (154LL - (long long )d1old)
+ (long long )x >= 0LL) && (155LL - (long long )d2) + (long long )x >= 0LL)
&& (156LL - (long long )d1) + (long long )x >= 0LL) && (-2LL + (long long
)d1) - (long long )d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2
>= 0LL) && (155LL - (long long )d1old) - (long long )d2 >= 0LL) && (156LL
- (long long )d1) - (long long )d1old >= 0LL) && (157LL - (long long )d1)
- (long long )d2 >= 0LL) && d1 == 79) && d2 == 78) && d1old == 77))) || ((((((((((((((((((-77
<= x && x <= 2147483347) && (-155LL + (long long )d1) + (long long )d2 >=
0LL) && (-155LL + (long long )d1old) + (long long )d2 >= 0LL) && (-154LL +
(long long )d1) + (long long )d1old >= 0LL) && (-1LL - (long long )d1) + (long
long )d2 >= 0LL) && (0LL - (long long )d1) + (long long )d1old >= 0LL) &&
(154LL - (long long )d1) + (long long )x >= 0LL) && (154LL - (long long )d1old)
+ (long long )x >= 0LL) && (155LL - (long long )d2) + (long long )x >= 0LL)
&& (long long )d1 + (long long )x >= 0LL) && (1LL + (long long )d1) - (long
long )d2 >= 0LL) && (154LL - (long long )d1) - (long long )d1old >= 0LL) &&
(155LL - (long long )d1) - (long long )d2 >= 0LL) && (155LL - (long long )d1old)
- (long long )d2 >= 0LL) && (long long )d1 - (long long )d1old >= 0LL) &&
d1 == 77) && d2 == 78) && d1old == 77)) || ((((((((((((((((((-75 <= x && x
<= 2147483424) && (-153LL + (long long )d1) + (long long )d2 >= 0LL) && (-152LL
+ (long long )d1) + (long long )d1old >= 0LL) && (-151LL + (long long )d1old)
+ (long long )d2 >= 0LL) && (-2LL + (long long )d1) + (long long )x >= 0LL)
&& (1LL - (long long )d1) + (long long )d2 >= 0LL) && (2LL - (long long )d1)
+ (long long )d1old >= 0LL) && (150LL - (long long )d1old) + (long long )x
>= 0LL) && (151LL - (long long )d2) + (long long )x >= 0LL) && (152LL - (long
long )d1) + (long long )x >= 0LL) && (-2LL + (long long )d1) - (long long
)d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2 >= 0LL) && (151LL
- (long long )d1old) - (long long )d2 >= 0LL) && (152LL - (long long )d1)
- (long long )d1old >= 0LL) && (153LL - (long long )d1) - (long long )d2 >=
0LL) && d1 == 77) && d2 == 76) && d1old == 75)) || ((((((((((((((((((-75 <=
x && x <= 2147483499) && (-151LL + (long long )d1) + (long long )d2 >= 0LL)
&& (-151LL + (long long )d1old) + (long long )d2 >= 0LL) && (-150LL + (long
long )d1) + (long long )d1old >= 0LL) && (-1LL - (long long )d1) + (long long
)d2 >= 0LL) && (0LL - (long long )d1) + (long long )d1old >= 0LL) && (150LL
- (long long )d1) + (long long )x >= 0LL) && (150LL - (long long )d1old) +
(long long )x >= 0LL) && (151LL - (long long )d2) + (long long )x >= 0LL)
&& (long long )d1 + (long long )x >= 0LL) && (1LL + (long long )d1) - (long
long )d2 >= 0LL) && (150LL - (long long )d1) - (long long )d1old >= 0LL) &&
(151LL - (long long )d1) - (long long )d2 >= 0LL) && (151LL - (long long )d1old)
- (long long )d2 >= 0LL) && (long long )d1 - (long long )d1old >= 0LL) &&
d1 == 75) && d2 == 76) && d1old == 75)) || (((((((((((((((((((-73 <= x &&
x <= 2147483574) && (-149LL + (long long )d1) + (long long )d2 >= 0LL) &&
(-148LL + (long long )d1) + (long long )d1old >= 0LL) && (-147LL + (long long
)d1old) + (long long )d2 >= 0LL) && (-2LL + (long long )d1) + (long long )x
>= 0LL) && (1LL - (long long )d1) + (long long )d2 >= 0LL) && (2LL - (long
long )d1) + (long long )d1old >= 0LL) && (146LL - (long long )d1old) + (long
long )x >= 0LL) && (147LL - (long long )d2) + (long long )x >= 0LL) && (148LL
- (long long )d1) + (long long )x >= 0LL) && (-2LL + (long long )d1) - (long
long )d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2 >= 0LL) &&
(147LL - (long long )d1old) - (long long )d2 >= 0LL) && (148LL - (long long
)d1) - (long long )d1old >= 0LL) && (149LL - (long long )d1) - (long long
)d2 >= 0LL) && 73 == d1old) && d1 == 75) && d2 == 74) && d1old == 73))) ||
((((((((((((((((-147LL + (long long )d1) + (long long )d2 >= 0LL && (2147483574LL
+ (long long )d1old) + (long long )d2 >= 0LL) && (2147483575LL + (long long
)d1) + (long long )d1old >= 0LL) && (-1LL - (long long )d1) + (long long )d2
>= 0LL) && (2147483573LL - (long long )d1old) + (long long )d2 >= 0LL) &&
(2147483721LL - (long long )d1) + (long long )d1old >= 0LL) && (1LL + (long
long )d1) - (long long )d2 >= 0LL) && (2147483574LL + (long long )d1) - (long
long )d1old >= 0LL) && (2147483722LL + (long long )d1old) - (long long )d2
>= 0LL) && (147LL - (long long )d1) - (long long )d2 >= 0LL) && (2147483720LL
- (long long )d1) - (long long )d1old >= 0LL) && (2147483721LL - (long long
)d1old) - (long long )d2 >= 0LL) && 73 == d1) && 74 == d2) && d1 == 73) &&
d2 == 74)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
13 |
2023-12-01T03:55:46+01:00 |
|