From d52d9e33edf9fafc3efeef09430e25a24af22f1c Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Wed, 14 Oct 2020 12:10:11 -0700 Subject: [PATCH] Added non-NULL assumptions to hash_iterator_string_string_generator and hash_find_string_string_generator --- verification/cbmc/stubs/hash_table_generators.c | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/verification/cbmc/stubs/hash_table_generators.c b/verification/cbmc/stubs/hash_table_generators.c index 71b18cd33..ad92e95a1 100644 --- a/verification/cbmc/stubs/hash_table_generators.c +++ b/verification/cbmc/stubs/hash_table_generators.c @@ -20,7 +20,9 @@ void hash_iterator_string_string_generator(struct aws_hash_iter *new_iter, const (void)old_iter; if (new_iter->status == AWS_HASH_ITER_STATUS_READY_FOR_USE) { new_iter->element.key = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(new_iter->element.key != NULL); new_iter->element.value = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(new_iter->element.value != NULL); } } @@ -32,8 +34,12 @@ void hash_find_string_string_generator( const struct aws_hash_table *map, const void *key, struct aws_hash_element *p_elem) { - p_elem->key = ensure_string_is_allocated_nondet_length(); - p_elem->value = ensure_string_is_allocated_nondet_length(); + if (p_elem) { + p_elem->key = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(p_elem->key != NULL); + p_elem->value = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(p_elem->value != NULL); + } } /**