# -*- mode: makefile -*-
# The first line sets the emacs major mode to Makefile

# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: Apache-2.0

################################################################
# Use this file to give project-specific definitions of the command
# line arguments to pass to CBMC tools like goto-cc to build the goto
# binaries and cbmc to do the property and coverage checking.
#
# Use this file to override most default definitions of variables in
# Makefile.common.
################################################################

# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
# COMPILE_FLAGS =

# Flags to pass to goto-cc for linking (typically those passed to gcc)
# LINK_FLAGS =

# Preprocessor include paths -I...
# Consider adding
#     INCLUDES += -I$(CBMC_ROOT)/include
# You will want to decide what order that comes in relative to the other
# include directories in your project.
#
# INCLUDES =

# order is important, we want proof includes first
INCLUDES += -I$(SRCDIR)/verification/cbmc/include # helper-inc
INCLUDES += -I$(SRCDIR)/verification/cbmc/aws-c-common/verification/cbmc/include # c-common-helper-inc
INCLUDES += -I$(SRCDIR)/include # c-enc-sdk-inc
INCLUDES += -I$(SRCDIR)/verification/cbmc/aws-c-common/include # c-common-inc

# Path to AWS-C-Common dependencies
COMMON_PROOF_SOURCE ?= $(abspath $(CBMC_ROOT)/aws-c-common/verification/cbmc/sources)
COMMON_PROOF_STUB ?= $(abspath $(CBMC_ROOT)/aws-c-common/verification/cbmc/stubs)
COMMON_PROOF_UNINLINE ?= $(abspath $(CBMC_ROOT)/aws-c-common/verification/cbmc/uninline)

# Preprocessor definitions -D...
# DEFINES =

# Path to arpa executable
# ARPA =

# Flags to pass to cmake for building the project
# ARPA_CMAKE_FLAGS =

# We override abort() to be assert(0), as it is not caught by
# CBMC as a violation
PROOF_SOURCES += $(COMMON_PROOF_STUB)/abort_override_assert_false.c
REMOVE_FUNCTION_BODY += abort