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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
#include <aws/common/hash_table.h>
#include <aws/common/math.h>
#include <aws/common/private/hash_table_impl.h>
#include <aws/common/string.h>
#include <limits.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/utils.h>
#include <stdio.h>
#include <stdlib.h>
/**
* Attempts to locate an element at key. If no such element was found,
* creates a new element, with value initialized to NULL. In either case, a
* pointer to the element is placed in *p_elem.
*
* If was_created is non-NULL, *was_created is set to 0 if an existing
* element was found, or 1 is a new element was created.
*
* Returns AWS_OP_SUCCESS if an item was found or created.
* Raises AWS_ERROR_OOM if hash table expansion was required and memory
* allocation failed.
*/
struct hash_table_entry *__CPROVER_file_local_hash_table_c_s_emplace_item(
struct hash_table_state *state,
struct hash_table_entry entry,
size_t probe_idx) {
AWS_PRECONDITION(hash_table_state_is_valid(state), "Input hash_table_state [state] must be valid.");
if (entry.hash_code == 0) {
AWS_POSTCONDITION(hash_table_state_is_valid(state), "Output hash_table_state [state] must be valid.");
return NULL;
}
size_t index;
__CPROVER_assume(index < state->size);
__CPROVER_assume(state->slots[index].hash_code == 0);
state->slots[index] = entry;
size_t empty_slot_idx;
__CPROVER_assume(hash_table_state_has_an_empty_slot(state, &empty_slot_idx));
AWS_POSTCONDITION(hash_table_state_is_valid(state), "Output hash_table_state [state] must be valid.");
return &state->slots[index];
}
|
