Line data    Source code

       1             : #include <aws/common/hash_table.h>
       2             : #include <aws/common/private/hash_table_impl.h>
       3             : 
       4             : #include <seahorn/seahorn.h>
       5             : 
       6             : #include <config.h>
       7             : #include <hash_table_helper.h>
       8             : #include <utils.h>
       9             : 
      10      150000 : int main(void) {
      11      150000 :   struct aws_hash_table map;
      12      150000 :   initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
      13      150000 :   assume(aws_hash_table_is_valid(&map));
      14      150000 :   map.p_impl->destroy_key_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
      15      150000 :   map.p_impl->destroy_value_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
      16      150000 : 
      17      150000 :   size_t empty_slot_idx;
      18      150000 :   assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx));
      19      150000 : 
      20      150000 :   void *key = nd_voidp();
      21      150000 :   void *value = nd_voidp();
      22      150000 :   bool track_was_created = nd_bool();
      23      150000 :   int was_created;
      24      150000 :   struct hash_table_state old_state = *map.p_impl;
      25      150000 : 
      26      150000 :   int rval = aws_hash_table_put(&map, key, value,
      27      150000 :                                 track_was_created ? &was_created : NULL);
      28      150000 :   if (rval == AWS_OP_SUCCESS) {
      29           0 :     if (track_was_created) {
      30           0 :       sassert(map.p_impl->entry_count == old_state.entry_count + was_created);
      31           0 :     } else {
      32           0 :       sassert(map.p_impl->entry_count == old_state.entry_count ||
      33           0 :               map.p_impl->entry_count == old_state.entry_count + 1);
      34           0 :     }
      35      150000 :   } else {
      36      150000 :     sassert(map.p_impl->entry_count == old_state.entry_count);
      37      150000 :   }
      38      150000 : 
      39      150000 :   return 0;
      40      150000 : }