False alarms for AWS C Common tasks
For several of the AWS C Common tasks, the -svcomp20
configuration of CPAchecker reports false alarms.
List of affected tasks:
aws-c-common/aws_add_size_checked_harness.yml
aws-c-common/aws_add_size_saturating_harness.yml
aws-c-common/aws_array_eq_c_str_harness.yml
aws-c-common/aws_array_list_capacity_harness.yml
aws-c-common/aws_array_list_clean_up_harness.yml
aws-c-common/aws_array_list_clear_harness.yml
aws-c-common/aws_array_list_comparator_string_harness.yml
aws-c-common/aws_array_list_init_dynamic_harness.yml
aws-c-common/aws_array_list_init_static_harness.yml
aws-c-common/aws_array_list_length_harness.yml
aws-c-common/aws_array_list_sort_harness.yml
aws-c-common/aws_array_list_swap_harness.yml
aws-c-common/aws_byte_buf_eq_c_str_harness.yml
aws-c-common/aws_byte_buf_from_c_str_harness.yml
aws-c-common/aws_byte_buf_reserve_relative_harness.yml
aws-c-common/aws_byte_buf_reset_harness.yml
aws-c-common/aws_byte_buf_secure_zero_harness.yml
aws-c-common/aws_byte_buf_write_from_whole_string_harness.yml
aws-c-common/aws_byte_buf_write_harness.yml
aws-c-common/aws_byte_cursor_from_c_str_harness.yml
aws-c-common/aws_hash_callback_c_str_eq_harness.yml
aws-c-common/aws_hash_table_init_bounded_harness.yml
aws-c-common/aws_is_power_of_two_harness.yml
aws-c-common/aws_linked_list_node_reset_harness.yml
aws-c-common/aws_linked_list_remove_harness.yml
aws-c-common/aws_mul_size_checked_harness.yml
aws-c-common/aws_mul_size_saturating_harness.yml
aws-c-common/aws_priority_queue_init_dynamic_harness.yml
aws-c-common/aws_ring_buffer_buf_belongs_to_pool_harness.yml
aws-c-common/aws_ring_buffer_init_harness.yml
aws-c-common/aws_ring_buffer_release_harness.yml
aws-c-common/aws_round_up_to_power_of_two_harness.yml
aws-c-common/aws_string_compare_harness.yml
aws-c-common/aws_string_eq_byte_buf_harness.yml
aws-c-common/aws_string_eq_byte_cursor_harness.yml
aws-c-common/aws_string_eq_harness.yml
aws-c-common/aws_string_new_from_array_harness.yml
aws-c-common/aws_string_new_from_c_str_harness.yml
aws-c-common/aws_string_new_from_string_harness.yml
aws-c-common/memset_override_0_harness.yml
Those that I checked all had extern functions like memset
, memcmp
, or __builtin_uaddl_overflow
. This might be related to missing implementations of these functions.
Edited by Philipp Wendler