./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/aws_array_list_length_harness_negated.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/aws_array_list_length_harness_negated.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2337:5-2343:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2882:5-2901:5 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2922:9-2943:9 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3200:5-3200:57 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3307:5-3307:57 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5002:5-5002:57 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5076:5-5089:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7027:5-7034:5 with factor 7
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7518:5-7524:5 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Imprecise][Unsound] Function definition missing for __atomic_exchange_n
[Info][Witness] couldn't parse entry: find uuid
[Info][Imprecise] Invalidating expressions: & c (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:255:12-255:46)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:255:12-255:46)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:255:12-255:46)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2498:5-2498:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7174:9-7174:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3493:5-3493:55)
[Warning][Deadcode] Function 'my_abort' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:232:1-234:1)
[Warning][Deadcode] Function '__CPROVER_allocated_memory' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:235:1-235:80)
[Warning][Deadcode] Function '__CPROVER_uninterpreted_hasher' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:238:1-238:84)
[Warning][Deadcode] Function '__CPROVER_uninterpreted_equals' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:239:1-239:96)
[Warning][Deadcode] Function '__CPROVER_uninterpreted_compare' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:240:1-240:116)
[Warning][Deadcode] Function '__CPROVER_overflow_plus' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:248:1-251:1)
[Warning][Deadcode] Function 'nondet_int' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:262:1-262:52)
[Warning][Deadcode] Function 'nondet_uint16_t' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:264:1-264:64)
[Warning][Deadcode] Function 'nondet_uint32_t' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:265:1-265:63)
[Warning][Deadcode] Function 'nondet_uint64_t' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:266:1-266:64)
[Warning][Deadcode] Function 'nondet_uint8_t' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:267:1-267:62)
[Warning][Deadcode] Function 'nondet_voidp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:268:1-268:66)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:1109:1-1113:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:1114:1-1118:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:1119:1-1123:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:1125:1-1129:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:1131:1-1135:1)
[Warning][Deadcode] Function 'aws_is_mem_zeroed' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2331:1-2348:1)
[Warning][Deadcode] Function 'aws_mul_u64_saturating' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2483:1-2489:1)
[Warning][Deadcode] Function 'aws_mul_u32_saturating' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2505:1-2511:1)
[Warning][Deadcode] Function 'aws_mul_u32_checked' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2517:1-2522:1)
[Warning][Deadcode] Function 'aws_add_u64_saturating' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2527:1-2533:1)
[Warning][Deadcode] Function 'aws_add_u64_checked' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2539:1-2544:1)
[Warning][Deadcode] Function 'aws_add_u32_saturating' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2549:1-2555:1)
[Warning][Deadcode] Function 'aws_add_u32_checked' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2561:1-2566:1)
[Warning][Deadcode] Function 'aws_mul_size_saturating' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2570:1-2578:1)
[Warning][Deadcode] Function 'aws_add_size_saturating' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2597:1-2605:1)
[Warning][Deadcode] Function 'aws_add_size_checked' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2611:1-2619:1)
[Warning][Deadcode] Function 'aws_is_power_of_two' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2624:1-2629:1)
[Warning][Deadcode] Function 'aws_round_up_to_power_of_two' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2635:1-2656:1)
[Warning][Deadcode] Function 's_can_fail_calloc_allocator' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2730:1-2733:1)
[Warning][Deadcode] Function 's_can_fail_malloc_allocator' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2739:1-2742:1)
[Warning][Deadcode] Function 's_can_fail_free_allocator' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2747:1-2750:1)
[Warning][Deadcode] Function 's_can_fail_realloc_allocator' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2756:1-2760:1)
[Warning][Deadcode] Function 'bounded_calloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2769:1-2776:1)
[Warning][Deadcode] Function 'can_fail_calloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2789:1-2793:1)
[Warning][Deadcode] Function 'can_fail_malloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2795:1-2799:1)
[Warning][Deadcode] Function 'can_fail_realloc' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2800:1-2817:1)
[Warning][Deadcode] Function 'aws_allocator_is_valid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2819:1-2822:1)
[Warning][Deadcode] Function 'aws_mem_acquire' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2824:1-2834:1)
[Warning][Deadcode] Function 'aws_mem_calloc' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2836:1-2856:1)
[Warning][Deadcode] Function 'aws_mem_acquire_many' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2860:1-2953:1)
[Warning][Deadcode] Function 'aws_mem_release' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2957:1-2970:1)
[Warning][Deadcode] Function 'aws_mem_realloc' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:2972:1-2994:1)
[Warning][Deadcode] Function 'aws_array_list_init_dynamic' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3185:1-3228:1)
[Warning][Deadcode] Function 'aws_array_list_init_static' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3230:1-3257:1)
[Warning][Deadcode] Function 'aws_array_list_debug_print' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3288:1-3298:1)
[Warning][Deadcode] Function 'aws_array_list_clean_up' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3300:1-3308:1)
[Warning][Deadcode] Function 'aws_array_list_push_back' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3310:1-3326:1)
[Warning][Deadcode] Function 'aws_array_list_front' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3328:1-3343:1)
[Warning][Deadcode] Function 'aws_array_list_pop_front' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3345:1-3356:1)
[Warning][Deadcode] Function 'aws_array_list_pop_front_n' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3358:1-3378:1)
[Warning][Deadcode] Function 'aws_array_list_erase' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3380:1-3409:1)
[Warning][Deadcode] Function 'aws_array_list_back' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3411:1-3427:1)
[Warning][Deadcode] Function 'aws_array_list_pop_back' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3429:1-3446:1)
[Warning][Deadcode] Function 'aws_array_list_clear' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3448:1-3458:1)
[Warning][Deadcode] Function 'aws_array_list_swap_contents' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3460:1-3476:1)
[Warning][Deadcode] Function 'aws_array_list_capacity' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3478:1-3485:1)
[Warning][Deadcode] Function 'aws_array_list_get_at' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3500:1-3513:1)
[Warning][Deadcode] Function 'aws_array_list_get_at_ptr' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3515:1-3528:1)
[Warning][Deadcode] Function 'aws_array_list_set_at' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3530:1-3559:1)
[Warning][Deadcode] Function 'aws_array_list_sort' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3561:1-3568:1)
[Warning][Deadcode] Function 'aws_is_big_endian' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4269:1-4272:1)
[Warning][Deadcode] Function 'aws_hton64' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4277:1-4292:1)
[Warning][Deadcode] Function 'aws_ntoh64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4297:1-4299:1)
[Warning][Deadcode] Function 'aws_hton32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4304:1-4310:1)
[Warning][Deadcode] Function 'aws_htonf32' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4315:1-4331:1)
[Warning][Deadcode] Function 'aws_htonf64' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4336:1-4356:1)
[Warning][Deadcode] Function 'aws_ntoh32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4361:1-4367:1)
[Warning][Deadcode] Function 'aws_ntohf32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4372:1-4374:1)
[Warning][Deadcode] Function 'aws_ntohf64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4379:1-4381:1)
[Warning][Deadcode] Function 'aws_hton24' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4386:1-4393:1)
[Warning][Deadcode] Function 'aws_ntoh24' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4398:1-4405:1)
[Warning][Deadcode] Function 'aws_hton16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4410:1-4416:1)
[Warning][Deadcode] Function 'aws_ntoh16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4421:1-4427:1)
[Warning][Deadcode] Function 'aws_linked_list_node_reset' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:4998:1-5004:1)
[Warning][Deadcode] Function 'aws_linked_list_empty' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5005:1-5010:1)
[Warning][Deadcode] Function 'aws_linked_list_is_valid' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5015:1-5034:1)
[Warning][Deadcode] Function 'aws_linked_list_node_next_is_valid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5041:1-5045:1)
[Warning][Deadcode] Function 'aws_linked_list_node_prev_is_valid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5052:1-5056:1)
[Warning][Deadcode] Function 'aws_linked_list_is_valid_deep' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5057:1-5091:1)
[Warning][Deadcode] Function 'aws_linked_list_init' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5096:1-5108:1)
[Warning][Deadcode] Function 'aws_linked_list_begin' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5113:1-5119:1)
[Warning][Deadcode] Function 'aws_linked_list_end' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5124:1-5130:1)
[Warning][Deadcode] Function 'aws_linked_list_rbegin' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5137:1-5143:1)
[Warning][Deadcode] Function 'aws_linked_list_rend' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5149:1-5155:1)
[Warning][Deadcode] Function 'aws_linked_list_next' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5160:1-5167:1)
[Warning][Deadcode] Function 'aws_linked_list_prev' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5172:1-5179:1)
[Warning][Deadcode] Function 'aws_linked_list_insert_after' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5184:1-5199:1)
[Warning][Deadcode] Function 'aws_linked_list_swap_nodes' is uncalled: 19 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5204:1-5230:1)
[Warning][Deadcode] Function 'aws_linked_list_insert_before' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5235:1-5250:1)
[Warning][Deadcode] Function 'aws_linked_list_remove' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5256:1-5263:1)
[Warning][Deadcode] Function 'aws_linked_list_push_back' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5268:1-5276:1)
[Warning][Deadcode] Function 'aws_linked_list_back' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5281:1-5289:1)
[Warning][Deadcode] Function 'aws_linked_list_pop_back' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5294:1-5302:1)
[Warning][Deadcode] Function 'aws_linked_list_push_front' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5307:1-5315:1)
[Warning][Deadcode] Function 'aws_linked_list_front' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5320:1-5328:1)
[Warning][Deadcode] Function 'aws_linked_list_pop_front' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5333:1-5341:1)
[Warning][Deadcode] Function 'aws_linked_list_swap_contents' is uncalled: 19 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5343:1-5370:1)
[Warning][Deadcode] Function 'aws_atomic_load_int' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5975:1-5978:1)
[Warning][Deadcode] Function 'aws_atomic_load_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5983:1-5986:1)
[Warning][Deadcode] Function 'aws_atomic_store_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5991:1-5994:1)
[Warning][Deadcode] Function 'aws_atomic_store_ptr' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:5999:1-6002:1)
[Warning][Deadcode] Function 'aws_atomic_exchange_int' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6008:1-6011:1)
[Warning][Deadcode] Function 'aws_atomic_exchange_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6017:1-6020:1)
[Warning][Deadcode] Function 'aws_atomic_compare_exchange_int' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6027:1-6033:1)
[Warning][Deadcode] Function 'aws_atomic_compare_exchange_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6040:1-6046:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_add' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6052:1-6055:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_sub' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6061:1-6064:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_and' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6070:1-6073:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_or' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6079:1-6082:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_xor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6088:1-6091:1)
[Warning][Deadcode] Function 'aws_atomic_priv_xlate_order' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6106:1-6121:1)
[Warning][Deadcode] Function 'aws_atomic_init_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6127:1-6130:1)
[Warning][Deadcode] Function 'aws_atomic_init_ptr' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6136:1-6139:1)
[Warning][Deadcode] Function 'aws_atomic_load_int_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6144:1-6147:1)
[Warning][Deadcode] Function 'aws_atomic_load_ptr_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6152:1-6155:1)
[Warning][Deadcode] Function 'aws_atomic_store_int_explicit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6160:1-6163:1)
[Warning][Deadcode] Function 'aws_atomic_store_ptr_explicit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6168:1-6171:1)
[Warning][Deadcode] Function 'aws_atomic_exchange_int_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6177:1-6183:1)
[Warning][Deadcode] Function 'aws_atomic_exchange_ptr_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6189:1-6195:1)
[Warning][Deadcode] Function 'aws_atomic_compare_exchange_int_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6202:1-6220:1)
[Warning][Deadcode] Function 'aws_atomic_compare_exchange_ptr_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6227:1-6245:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_add_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6250:1-6253:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_sub_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6258:1-6261:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_or_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6266:1-6269:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_and_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6274:1-6277:1)
[Warning][Deadcode] Function 'aws_atomic_fetch_xor_explicit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6282:1-6285:1)
[Warning][Deadcode] Function 'aws_atomic_thread_fence' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6291:1-6294:1)
[Warning][Deadcode] Function 'aws_ring_buffer_check_atomic_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6400:1-6406:1)
[Warning][Deadcode] Function 'aws_ring_buffer_is_empty' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6411:1-6417:1)
[Warning][Deadcode] Function 'aws_ring_buffer_is_valid' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6423:1-6442:1)
[Warning][Deadcode] Function 'aws_string_bytes' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6603:1-6607:1)
[Warning][Deadcode] Function 'aws_string_is_valid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6613:1-6618:1)
[Warning][Deadcode] Function 'aws_c_string_is_valid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6623:1-6633:1)
[Warning][Deadcode] Function 'aws_byte_buf_is_bounded' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6905:1-6908:1)
[Warning][Deadcode] Function 'aws_byte_buf_has_allocator' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6911:1-6914:1)
[Warning][Deadcode] Function 'ensure_byte_buf_has_allocated_buffer_member' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6916:1-6921:1)
[Warning][Deadcode] Function 'ensure_ring_buffer_has_allocated_members' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6923:1-6933:1)
[Warning][Deadcode] Function 'ensure_byte_buf_has_allocated_buffer_member_in_range' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6938:1-6947:1)
[Warning][Deadcode] Function 'ensure_byte_buf_has_allocated_buffer_member_in_ring_buf' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6952:1-6971:1)
[Warning][Deadcode] Function 'aws_byte_cursor_is_bounded' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6974:1-6977:1)
[Warning][Deadcode] Function 'ensure_byte_cursor_has_allocated_buffer_member' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:6979:1-6983:1)
[Warning][Deadcode] Function 'ensure_linked_list_is_allocated' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7014:1-7038:1)
[Warning][Deadcode] Function 'aws_priority_queue_is_bounded' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7041:1-7059:1)
[Warning][Deadcode] Function 'ensure_priority_queue_has_allocated_members' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7061:1-7065:1)
[Warning][Deadcode] Function 'ensure_hash_table_has_valid_destroy_functions' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7067:1-7074:1)
[Warning][Deadcode] Function 'aws_hash_table_has_an_empty_slot' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7077:1-7080:1)
[Warning][Deadcode] Function 'hash_table_state_has_an_empty_slot' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7083:1-7090:1)
[Warning][Deadcode] Function 'hash_proof_destroy_noop' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7098:1-7098:40)
[Warning][Deadcode] Function 'ensure_string_is_allocated_nondet_length' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7100:1-7105:1)
[Warning][Deadcode] Function 'ensure_string_is_allocated_bounded_length' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7107:1-7111:1)
[Warning][Deadcode] Function 'ensure_string_is_allocated' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7113:1-7123:1)
[Warning][Deadcode] Function 'ensure_c_str_is_allocated' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7125:1-7134:1)
[Warning][Deadcode] Function 'assert_bytes_match' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7135:1-7148:1)
[Warning][Deadcode] Function 'assert_all_bytes_are' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7150:1-7158:1)
[Warning][Deadcode] Function 'assert_all_zeroes' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7160:1-7162:1)
[Warning][Deadcode] Function 'assert_byte_from_buffer_matches' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7164:1-7168:1)
[Warning][Deadcode] Function 'assert_byte_buf_equivalence' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7197:1-7213:1)
[Warning][Deadcode] Function 'assert_byte_cursor_equivalence' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7215:1-7226:1)
[Warning][Deadcode] Function 'assert_ring_buffer_equivalence' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7228:1-7240:1)
[Warning][Deadcode] Function 'check_hash_table_unchanged' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7242:1-7246:1)
[Warning][Deadcode] Function 'nondet_compare' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7248:1-7252:1)
[Warning][Deadcode] Function 'uninterpreted_compare' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7255:1-7268:1)
[Warning][Deadcode] Function 'nondet_equals' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7271:1-7276:1)
[Warning][Deadcode] Function 'uninterpreted_equals' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7287:1-7301:1)
[Warning][Deadcode] Function 'uninterpreted_equals_assert_inputs_nonnull' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7304:1-7309:1)
[Warning][Deadcode] Function 'nondet_hasher' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7311:1-7314:1)
[Warning][Deadcode] Function 'uninterpreted_hasher' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7319:1-7322:1)
[Warning][Deadcode] Function 'aws_last_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7340:1-7342:1)
[Warning][Deadcode] Function 'aws_array_list_calc_necessary_size' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7355:1-7369:1)
[Warning][Deadcode] Function 'aws_array_list_shrink_to_fit' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7371:1-7404:1)
[Warning][Deadcode] Function 'aws_array_list_copy' is uncalled: 31 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7406:1-7454:1)
[Warning][Deadcode] Function 'aws_array_list_ensure_capacity' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7456:1-7507:1)
[Warning][Deadcode] Function 'aws_array_list_mem_swap' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7509:1-7530:1)
[Warning][Deadcode] Function 'aws_array_list_swap' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7532:1-7551:1)
[Warning][Deadcode] Function 'aws_secure_zero' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7710:1-7727:1)
[Warning][Deadcode] Function 'aws_common_fatal_assert_library_initialized' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7909:1-7918:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'assert_array_list_equivalence' has dead code:
  on line 7184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7184-7184)
  on lines 7188..7193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7188-7193)
  on line 7195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7195-7195)
[Warning][Deadcode] Function 'aws_array_list_is_valid' has dead code:
  on line 3265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3265-3265)
[Warning][Deadcode] Function 'aws_array_list_length_harness' has dead code:
  on line 7939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7939-7939)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 76
  dead: 860 (850 in uncalled functions)
  total lines: 936
[Warning][Deadcode][CWE-571] condition 'storage' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7171:9-7171:37)
[Warning][Deadcode][CWE-570] condition '(unsigned long )lhs == (unsigned long )rhs' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7183:9-7183:19)
[Warning][Deadcode][CWE-571] condition 'lhs' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7186:9-7186:41)
[Warning][Deadcode][CWE-571] condition 'rhs' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:7186:9-7186:41)
[Warning][Deadcode][CWE-570] condition '! list' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/aws-c-common/aws_array_list_length_harness_negated.i:3263:9-3263:14)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
[Error][Imprecise][Unsound] Function definition missing
