aws_hash_ptr + aws_hash_c_string

Author: danielsn

.cbmc-batch/jobs/aws_hash_c_string/Makefile

@@ -0,0 +1,33 @@
+# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+#
+# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+# this file except in compliance with the License. A copy of the License is
+# located at
+#
+#     http://aws.amazon.com/apache2.0/
+#
+# or in the "license" file accompanying this file. This file is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+# implied. See the License for the specific language governing permissions and
+# limitations under the License.
+
+###########
+MAX_STRING_SIZE ?= 4
+DEFINES += -DMAX_STRING_SIZE=$(MAX_STRING_SIZE) 
+
+UNWINDSET += strlen.0:$(shell echo $$(( $(MAX_STRING_SIZE) + 1)))
+
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+
+ENTRY = aws_hash_c_string_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_hash_c_string/aws_hash_c_string_harness.c

@@ -0,0 +1,26 @@
+/*
+ * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+ * this file except in compliance with the License. A copy of the License is
+ * located at
+ *
+ *     http://aws.amazon.com/apache2.0/
+ *
+ * or in the "license" file accompanying this file. This file is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+ * implied. See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <aws/common/hash_table.h>
+#include <aws/common/private/hash_table_impl.h>
+#include <proof_helpers/make_common_data_structures.h>
+#include <proof_helpers/proof_allocators.h>
+#include <proof_helpers/utils.h>
+
+void aws_hash_c_string_harness() {
+  const char* str = make_arbitrary_c_str(MAX_STRING_SIZE);
+  /* This function has no pre or post conditions */
+  uint64_t rval = aws_hash_c_string(str);
+}

.cbmc-batch/jobs/aws_hash_c_string/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;strlen.0:5;--object-bits;8"
+goto: aws_hash_c_string_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_hash_ptr/Makefile

@@ -0,0 +1,26 @@
+# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+#
+# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+# this file except in compliance with the License. A copy of the License is
+# located at
+#
+#     http://aws.amazon.com/apache2.0/
+#
+# or in the "license" file accompanying this file. This file is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+# implied. See the License for the specific language governing permissions and
+# limitations under the License.
+
+###########
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+
+ENTRY = aws_hash_ptr_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_hash_ptr/aws_hash_ptr_harness.c

@@ -0,0 +1,29 @@
+/*
+ * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+ * this file except in compliance with the License. A copy of the License is
+ * located at
+ *
+ *     http://aws.amazon.com/apache2.0/
+ *
+ * or in the "license" file accompanying this file. This file is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+ * implied. See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <aws/common/hash_table.h>
+#include <aws/common/private/hash_table_impl.h>
+#include <proof_helpers/make_common_data_structures.h>
+#include <proof_helpers/proof_allocators.h>
+#include <proof_helpers/utils.h>
+
+/**
+ * Runtime: 4.5s
+ */
+void aws_hash_ptr_harness() {
+  void* ptr;
+  /* This function has no pre or post conditions */
+  uint64_t rval = aws_hash_ptr(ptr);
+}

.cbmc-batch/jobs/aws_hash_ptr/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+goto: aws_hash_ptr_harness.goto
+expected: "SUCCESSFUL"