Added README, removed unnecessary code, added dfcc to build

-- DFCC failing in this context

Author: Nathan Wetzler

regression/contracts/s2n_record_writev/Makefile

@@ -10,8 +10,8 @@ PROOFDIR ?= $(abspath .)
 
 CBMC_OBJECT_BITS = 9
 PROOF_UID = s2n_record_writev
-HARNESS_ENTRY = $(PROOF_UID)
-HARNESS_FILE = $(HARNESS_ENTRY).c
+HARNESS_ENTRY = $(PROOF_UID)_harness
+HARNESS_FILE = $(PROOF_UID).c
 
 CHECK_FUNCTION_CONTRACTS += s2n_record_writev
 USE_FUNCTION_CONTRACTS += s2n_hmac_update

regression/contracts/s2n_record_writev/Makefile.common

@@ -662,22 +662,8 @@ $(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
 	  --ci-stage build \
 	  --description "$(PROOF_UID): slicing global initializations"
 
-# Replace function calls with function contracts
-# This must be done before enforcing function contracts,
-# since contract enforcement inlines all function calls.
-$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
-	$(LITANI) add-job \
-	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
-	  --inputs $^ \
-	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/use_function_contracts-log.txt \
-	  --pipeline-name "$(PROOF_UID)" \
-	  --ci-stage build \
-	  --description "$(PROOF_UID): replacing function calls with function contracts"
-
 # Unwind loops for loop and function contracts
-$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
+$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)5.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
@@ -704,7 +690,7 @@ $(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
 $(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \

regression/contracts/s2n_record_writev/README

@@ -0,0 +1,9 @@
+This directory contains an example of a problem encountered when
+applying function contracts in the context of AWS s2n-tls.  Run the
+example by using the command:
+
+make veryclean && make result
+
+This creates a large problem during symbolic execution and solving.
+
+This test is currently not included in the any regression.