Updates aws_hash_table stubs for CBMC proofs #714
Conversation
…nd hash_find_string_string_generator
feliperodri
changed the title
| __CPROVER_assume(new_iter->element.key != NULL); | ||
| new_iter->element.value = ensure_string_is_allocated_nondet_length(); | ||
| __CPROVER_assume(new_iter->element.value != NULL); |
There was a problem hiding this comment.
Do we guarantee these assumptions in this function as well? What happens with the actual function?
There was a problem hiding this comment.
So there is no matching function corresponding to this stub. It's a generator to generate items in a hash table when it's iterated over (it's the HASH_ITER_ELEMENT_GENERATOR from the aws_hash_iter_override stubs). So whether it's guaranteed is I guess an assumption over the hash_table we're iterating over. But in general, some functions might require hash tables with this guarantee and some might not, so maybe we could have two functions? I'll also think of a way to add this as a precondition to the function itself.
There was a problem hiding this comment.
Could you create a GitHub issue to track whether we should map these as a precondition? @tegansb
There was a problem hiding this comment.
Made here #715. Could you add the cbmc label?
|
This changes has been merged in PR #716. |
Description of changes:
Updates the hash_iterator_string_string_generator and hash_find_string_string_generator functions with non-NULL assumptions.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.