Added notice, licensing info, DFCC fix

Author: Nathan Wetzler

regression/contracts/s2n_record_writev/Makefile.common

@@ -567,17 +567,17 @@ $(REWRITTEN_SOURCES):
 ################################################################
 # Build targets that make the relevant .goto files
 
-# Compile project sources
-$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
-	$(LITANI) add-job \
-	  --command \
-	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
-	  --inputs $^ \
-	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/project_sources-log.txt \
-	  --pipeline-name "$(PROOF_UID)" \
-	  --ci-stage build \
-	  --description "$(PROOF_UID): building project binary"
+# # Compile project sources
+# $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
+# 	$(LITANI) add-job \
+# 	  --command \
+# 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
+# 	  --inputs $^ \
+# 	  --outputs $@ \
+# 	  --stdout-file $(LOGDIR)/project_sources-log.txt \
+# 	  --pipeline-name "$(PROOF_UID)" \
+# 	  --ci-stage build \
+# 	  --description "$(PROOF_UID): building project binary"
 
 # Compile proof sources
 $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
@@ -591,20 +591,20 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
 	  --ci-stage build \
 	  --description "$(PROOF_UID): building proof binary"
 
-# Remove function bodies from project sources
-$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
-	$(LITANI) add-job \
-	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
-	  --inputs $^ \
-	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/remove_function_body-log.txt \
-	  --pipeline-name "$(PROOF_UID)" \
-	  --ci-stage build \
-	  --description "$(PROOF_UID): removing function bodies from project sources"
+# # Remove function bodies from project sources
+# $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
+# 	$(LITANI) add-job \
+# 	  --command \
+# 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
+# 	  --inputs $^ \
+# 	  --outputs $@ \
+# 	  --stdout-file $(LOGDIR)/remove_function_body-log.txt \
+# 	  --pipeline-name "$(PROOF_UID)" \
+# 	  --ci-stage build \
+# 	  --description "$(PROOF_UID): removing function bodies from project sources"
 
 # Link project and proof sources into the proof harness
-$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
+$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto
 	$(LITANI) add-job \
 	  --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
 	  --inputs $^ \
@@ -638,20 +638,20 @@ $(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
 	  --ci-stage build \
 	  --description "$(PROOF_UID): setting static variables to nondet"
 
-# Omit unused functions (sharpens coverage calculations)
-$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
-	$(LITANI) add-job \
-	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
-	  --inputs $^ \
-	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
-	  --pipeline-name "$(PROOF_UID)" \
-	  --ci-stage build \
-	  --description "$(PROOF_UID): dropping unused functions"
+# # Omit unused functions (sharpens coverage calculations)
+# $(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
+# 	$(LITANI) add-job \
+# 	  --command \
+# 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
+# 	  --inputs $^ \
+# 	  --outputs $@ \
+# 	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
+# 	  --pipeline-name "$(PROOF_UID)" \
+# 	  --ci-stage build \
+# 	  --description "$(PROOF_UID): dropping unused functions"
 
 # Omit initialization of unused global variables (reduces problem size)
-$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
+$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)3.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \

regression/contracts/s2n_record_writev/NOTICE

@@ -0,0 +1,2 @@
+s2n
+Copyright 2014-2015 Amazon.com, Inc. or its affiliates. All Rights Reserved.