1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
/**
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
* SPDX-License-Identifier: Apache-2.0.
*/
#include <aws/common/string.h>
#include <proof_helpers/nondet.h>
/**
* Override the aws_string_new_from_array to just give non-det bytes, rather than doing the memcpy.
* Since we already check AWS_MEM_IS_READABLE(bytes, len) in the precondition, this is sound - it overapproximates
* the behaviour of the real function, and has all the same memory safety checks.
*/
struct aws_string *aws_string_new_from_array(struct aws_allocator *allocator, const uint8_t *bytes, size_t len) {
AWS_PRECONDITION(allocator);
AWS_PRECONDITION(AWS_MEM_IS_READABLE(bytes, len));
size_t malloc_size = sizeof(struct aws_string) + 1 + len;
struct aws_string *str = malloc(malloc_size);
if (str == NULL) {
return NULL;
}
__CPROVER_assume(str->allocator == allocator);
__CPROVER_assume(str->len == len);
__CPROVER_assume(str->bytes[len] == '\0');
AWS_RETURN_WITH_POSTCONDITION(str, aws_string_is_valid(str));
}
|
