CBMC: Add proof for aws_string_new_from_buf

verification/cbmc/proofs/aws_string_new_from_buf/Makefile

@@ -0,0 +1,24 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0.
+
+include ../Makefile.aws_string
+include ../Makefile.aws_byte_buf
+
+CBMCFLAGS +=
+
+PROOF_UID = aws_string_new_from_buf
+HARNESS_ENTRY = $(PROOF_UID)_harness
+HARNESS_FILE = $(PROOFDIR)/$(HARNESS_ENTRY).c
+
+PROOF_SOURCES += $(HARNESS_FILE)
+PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
+PROJECT_SOURCES += $(SRCDIR)/source/allocator.c
+PROOF_SOURCES += $(PROOF_SOURCE)/utils.c
+PROOF_SOURCES += $(PROOF_STUB)/error.c
+
+PROJECT_SOURCES += $(SRCDIR)/source/byte_buf.c
+PROJECT_SOURCES += $(SRCDIR)/source/common.c
+PROJECT_SOURCES += $(SRCDIR)/source/string.c
+
+include ../Makefile.common
+

verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c

@@ -0,0 +1,33 @@
+/**
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0.
+ */
+
+#include <aws/common/byte_buf.h>
+#include <aws/common/string.h>
+#include <proof_helpers/make_common_data_structures.h>
+#include <proof_helpers/utils.h>
+
+void aws_string_new_from_buf_harness() {
+    /* parameters */
+    struct aws_allocator *allocator;
+    struct aws_byte_buf buf;
+
+    /* precondition */
+    ASSUME_DEFAULT_ALLOCATOR(allocator);
+    __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE));
+    ensure_byte_buf_has_allocated_buffer_member(&buf);
+    __CPROVER_assume(aws_byte_buf_is_valid(&buf));
+
+    /* operation under verification */
+    struct aws_string *str = aws_string_new_from_buf(allocator, &buf);
+
+    /* assertions */
+    if (str) {
+        assert(str->len == buf.len);
+        assert(str->bytes[str->len] == 0);
+        assert_bytes_match(str->bytes, buf.buffer, str->len);
+        assert(aws_string_is_valid(str));
+    }
+}
+

verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt

@@ -0,0 +1,2 @@
+This file marks the directory as containing a CBMC proof
+