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 :   /* data structure */
      12      150000 :   struct aws_hash_table map;
      13      150000 :   initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
      14      150000 :   assume(aws_hash_table_is_valid(&map));
      15      150000 : 
      16      150000 :   size_t empty_slot_idx;
      17      150000 :   assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx));
      18      150000 : 
      19      150000 :   struct store_byte_from_buffer old_byte;
      20      150000 :   save_byte_from_hash_table(&map, &old_byte);
      21      150000 : 
      22      150000 :   void *key = nd_voidp();
      23      150000 :   struct aws_hash_element elem;
      24      150000 :   struct aws_hash_element *p_elem = &elem;
      25      150000 : 
      26      150000 :   /* Preconditions */
      27      150000 :   assume(aws_hash_table_is_valid(&map));
      28      150000 :   assume(AWS_OBJECT_PTR_IS_WRITABLE(&p_elem));
      29      150000 : 
      30      150000 :   int rval = aws_hash_table_find(&map, key, &p_elem);
      31      150000 :   sassert(rval == AWS_OP_SUCCESS);
      32      150000 :   if (p_elem) {
      33           0 :     sassert(AWS_OBJECT_PTR_IS_READABLE(p_elem));
      34             : #ifdef __SEA_UNINTERP_FN__
      35             :     sassert(p_elem->key == key || uninterpreted_equals(p_elem->key, key));
      36             : #endif
      37             :   }
      38      150000 :   sassert(aws_hash_table_is_valid(&map));
      39      150000 :   assert_hash_table_unchanged(&map, &old_byte);
      40      150000 :   return 0;
      41      150000 : }