CBMC proof stubs do not replace included functions

[adpaco-aws]

In the aws_cryptosdk_keyring_release CBMC proof, a few stubs coming from stubs/ are added to proof sources but not able to replace the corresponding functions coming from INCLUDES. Below is the Makefile code.

# aws_atomic_fetch_sub_explicit receives a volatile input, which is always model
# as non-deterministic in CBMC; thus, we need a deterministic stub for it
PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_fetch_sub_explicit.c
REMOVE_FUNCTION_BODY += aws_atomic_fetch_sub_explicit

PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_load_int.c
REMOVE_FUNCTION_BODY += aws_atomic_load_int

PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_priv_xlate_order.c
REMOVE_FUNCTION_BODY += aws_atomic_priv_xlate_order

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c

HARNESS_ENTRY = aws_cryptosdk_keyring_release_harness
HARNESS_FILE = $(HARNESS_ENTRY).c

PROOF_SOURCES += $(HARNESS_FILE)

REMOVE_FUNCTION_BODY += hash_proof_destroy_noop
REMOVE_FUNCTION_BODY += aws_raise_error_private

We have tried to force removal by adding

REMOVE_FUNCTION_BODY += __CPROVER_file_local_atomics_gnu_inl_aws_atomic_fetch_sub_explicit$link5

which is the name given to the function already included. We have also tried with similar names with different escape sequences.

This could be related to #625

[feliperodri]

This functions come from aws_atomics_gnu.inl, which is not part of our uninline folder. We need to update AWS C Common to include this "uninline" file and them see if we can properly stub out these functions.