# -*- 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 targets, including targets
# that may depend on targets defined in Makefile.common.
################################################################

# Each proof requires core_json.c to be patched (using sed) and dumped into the
# proof directory. The exact sed invocation differs for each proof. So each
# proof must set the CORE_JSON_SED_EXPR variable, which this rule uses as the
# argument to sed.
$(PROOFDIR)/core_json.c: $(SRCDIR)/source/core_json.c
	$(LITANI) add-job \
	  --command \
	    "sed -E '$(CORE_JSON_SED_EXPR)' $^" \
	  --inputs $^ \
	  --outputs $@ \
	  --stdout-file $@ \
	  --ci-stage build \
	  --pipeline-name "$(PROOF_UID)" \
	  --description "$(PROOF_UID): patching core_json.c"