1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
# -*- mode: makefile -*-
# The first line sets the emacs major mode to Makefile
################################################################
# 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...
INCLUDES += -I$(CBMC_ROOT)/include
INCLUDES += -I$(CBMC_ROOT)/aws-verification-model-for-libcrypto/include
INCLUDES += -I$(SRCDIR)
INCLUDES += -I$(SRCDIR)/api
INCLUDES += -I$(SRCDIR)/crypto
# OpenSSL Model Source
OPENSSL_SOURCE = $(CBMC_ROOT)/aws-verification-model-for-libcrypto/source
# Preprocessor definitions -D...
# Whether a proof needs these checks should be decided on a proof by proof basis.
# Checks can be enabled by setting AWS_DEEP_CHECKS to 1 in the makefile
# of the proof that requires them
AWS_DEEP_CHECKS ?= 0
DEFINES += -DAWS_DEEP_CHECKS=$(AWS_DEEP_CHECKS)
# Extra CBMC flags not enabled by Makefile.common
# CHECKFLAGS += --enum-range-check
CHECKFLAGS += --pointer-primitive-check
################################################################
# Remove function bodies that are not used in the proofs.
# Removing the function from the goto program helps CBMC's
# function pointer analysis
# We override abort() to be assert(0)
PROOF_SOURCES += $(PROOF_STUB)/abort_override_assert_false.c
REMOVE_FUNCTION_BODY += abort
# Useful for setting unwind limits to one more than some value.
addone = $(shell echo $$(( $(1) + 1)))
|
