s2n_record_writev standalone example

Author: Nathan Wetzler

regression/contracts/s2n_record_writev/Makefile

@@ -0,0 +1,23 @@
+PROJECT_NAME = "s2n"
+
+CHECKFLAGS += --pointer-primitive-check
+
+
+LITANI ?= litani
+
+PROOFDIR ?= $(abspath .)
+
+
+CBMC_OBJECT_BITS = 9
+PROOF_UID = s2n_record_writev
+HARNESS_ENTRY = $(PROOF_UID)
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+CHECK_FUNCTION_CONTRACTS += s2n_record_writev
+USE_FUNCTION_CONTRACTS += s2n_hmac_update
+
+PROJECT_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
+
+
+include Makefile.common