45 lines
1.2 KiB
Plaintext
45 lines
1.2 KiB
Plaintext
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
|
# SPDX-License-Identifier: MIT
|
|
|
|
HARNESS_ENTRY=harness
|
|
|
|
ifdef CBMC_MAX_BUFSIZE
|
|
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
|
|
endif
|
|
ifdef THINGNAME_MAX_LENGTH
|
|
DEFINES += -DTHINGNAME_MAX_LENGTH=$(THINGNAME_MAX_LENGTH)
|
|
endif
|
|
ifdef JOBID_MAX_LENGTH
|
|
DEFINES += -DJOBID_MAX_LENGTH=$(JOBID_MAX_LENGTH)
|
|
endif
|
|
|
|
INCLUDES += -I$(CBMC_ROOT)/include
|
|
INCLUDES += -I$(SRCDIR)/source/include
|
|
|
|
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
|
|
PROJECT_SOURCES += $(PROOFDIR)/jobs.c
|
|
|
|
include ../Makefile.common
|
|
|
|
# remove static constraints to facilitate proofs
|
|
# replace some functions with stubs by renaming originals
|
|
# (see SED_EXPR in proof Makefiles)
|
|
|
|
# Command to pass to sed to patch jobs.c.
|
|
# The characters " and # must be escaped with backslash.
|
|
JOBS_SED_EXPR = 1s/^/\#include \"jobs_annex.h\" /; s/^static //; $(SED_EXPR)
|
|
|
|
$(PROOFDIR)/jobs.c: $(SRCDIR)/source/jobs.c
|
|
$(LITANI) add-job \
|
|
--command \
|
|
"sed -E '$(JOBS_SED_EXPR)' $^ > $@" \
|
|
--inputs $^ \
|
|
--outputs $@ \
|
|
--stdout-file $(LOGDIR)/jobs-log.txt \
|
|
--ci-stage build \
|
|
--pipeline-name "$(PROOF_UID)" \
|
|
--description "$(PROOF_UID): patching jobs.c"
|
|
|
|
cleanclean: veryclean
|
|
-$(RM) $(PROOFDIR)/jobs.c
|