LCOV - code coverage report
Current view: top level - seahorn/jobs/hash_table_remove - aws_hash_table_remove_harness.c (source / functions) Hit Total Coverage
Test: all_fuzz.info Lines: 31 37 83.8 %
Date: 2021-04-23 16:28:21 Functions: 1 1 100.0 %

          Line data    Source code
       1             : #include <aws/common/hash_table.h>
       2             : #include <aws/common/private/hash_table_impl.h>
       3             : 
       4             : #include <hash_table_helper.h>
       5             : #include <seahorn/seahorn.h>
       6             : #include <utils.h>
       7             : 
       8      150000 : int main(void) {
       9      150000 :   struct aws_hash_table map;
      10      150000 :   initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
      11      150000 :   assume(aws_hash_table_is_valid(&map));
      12      150000 :   map.p_impl->destroy_key_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
      13      150000 :   map.p_impl->destroy_value_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
      14      150000 : 
      15      150000 :   size_t empty_slot_idx;
      16      150000 :   assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx));
      17      150000 :   void *key = nd_voidp();
      18      150000 :   struct aws_hash_element p_elem;
      19      150000 :   bool get_p_elem = nd_bool();
      20      150000 :   bool track_was_present = nd_bool();
      21      150000 :   int was_present;
      22      150000 : 
      23      150000 :   struct hash_table_state old_state = *map.p_impl;
      24      150000 : 
      25      150000 :   /* assume the preconditions */
      26      150000 :   assume(aws_hash_table_is_valid(&map));
      27      150000 :   assume(AWS_OBJECT_PTR_IS_WRITABLE(&p_elem));
      28      150000 :   assume(AWS_OBJECT_PTR_IS_WRITABLE(&was_present));
      29      150000 : 
      30      150000 :   int rval = aws_hash_table_remove(&map, key, get_p_elem ? &p_elem : NULL,
      31      150000 :                                    track_was_present ? &was_present : NULL);
      32      150000 :   sassert(aws_hash_table_is_valid(&map));
      33      150000 :   if (rval == AWS_OP_SUCCESS) {
      34           0 :     if (track_was_present) {
      35           0 :       sassert(map.p_impl->entry_count == old_state.entry_count - was_present);
      36           0 :     } else {
      37           0 :       sassert(map.p_impl->entry_count == old_state.entry_count ||
      38           0 :               map.p_impl->entry_count == old_state.entry_count - 1);
      39           0 :     }
      40             : #ifdef __SEA_UNINTERP_FN__
      41             :     if (get_p_elem && track_was_present && was_present == 1) {
      42             :       sassert(uninterpreted_equals(p_elem.key, key));
      43             :     }
      44             : #endif
      45      150000 :   } else {
      46      150000 :     sassert(map.p_impl->entry_count == old_state.entry_count);
      47      150000 :   }
      48      150000 :   return 0;
      49      150000 : }

Generated by: LCOV version 1.13