Line data    Source code

       1             : #include <aws/common/hash_table.h>
       2             : #include <hash_table_helper.h>
       3             : #include <seahorn/seahorn.h>
       4             : #include <utils.h>
       5             : 
       6      150000 : int main(void) {
       7      150000 :   struct aws_hash_table to;
       8      150000 :   struct aws_hash_table from;
       9      150000 : 
      10      150000 : #if defined(__KLEE__) || defined(__FUZZ__)
      11      150000 :   initialize_bounded_aws_hash_table(&from, MAX_TABLE_SIZE);
      12             : #else
      13             :   // There are no loops in the code under test, so use the biggest possible
      14             :   // value
      15             :   initialize_bounded_aws_hash_table(&from, SIZE_MAX);
      16             : #endif
      17      150000 :   assume(aws_hash_table_is_valid(&from));
      18      150000 : 
      19      150000 :   struct store_byte_from_buffer stored_byte;
      20      150000 :   save_byte_from_hash_table(&from, &stored_byte);
      21      150000 : 
      22      150000 :   aws_hash_table_move(&to, &from);
      23      150000 : 
      24      150000 :   // Ensure that the destination table is valid.
      25      150000 :   sassert(aws_hash_table_is_valid(&to));
      26      150000 : 
      27      150000 :   // Ensure that the two tables were byte for byte swapped
      28      150000 :   assert_hash_table_unchanged(&to, &stored_byte);
      29      150000 :   return 0;
      30      150000 : }