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 :   /* element to be created */
      17      150000 :   size_t empty_slot_idx;
      18      150000 :   assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx));
      19      150000 :   void *key = nd_voidp();
      20      150000 :   struct aws_hash_element elm;
      21      150000 :   struct aws_hash_element *p_elem = &elm;
      22      150000 :   bool get_p_elem = nd_bool();
      23      150000 :   bool track_was_created = nd_bool();
      24      150000 :   int was_created; // for storing tracked result
      25      150000 : 
      26      150000 :   struct hash_table_state old_state = *map.p_impl;
      27      150000 : 
      28      150000 :   /* operation under verification*/
      29      150000 :   int rval = aws_hash_table_create(&map, key, get_p_elem ? &p_elem : NULL,
      30      150000 :                                    track_was_created ? &was_created : NULL);
      31      150000 : 
      32      150000 :   /* assertions */
      33      150000 :   sassert(aws_hash_table_is_valid(&map));
      34      150000 :   if (rval == AWS_OP_SUCCESS) {
      35           0 :     if (track_was_created) {
      36           0 :       sassert(map.p_impl->entry_count == old_state.entry_count + was_created);
      37           0 :     } else {
      38           0 :       sassert(map.p_impl->entry_count == old_state.entry_count ||
      39           0 :               map.p_impl->entry_count == old_state.entry_count + 1);
      40           0 :     }
      41             : #ifdef __SEA_UNINTERP_FN__
      42             :     if (get_p_elem) {
      43             :       sassert(uninterpreted_equals(p_elem->key, key));
      44             :     }
      45             : #endif
      46      150000 :   } else {
      47      150000 :     sassert(map.p_impl->entry_count == old_state.entry_count);
      48      150000 :   }
      49      150000 : 
      50      150000 :   return 0;
      51      150000 : }