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 a;
       8      150000 :   struct aws_hash_table b;
       9      150000 :   struct store_byte_from_buffer stored_byte_a;
      10      150000 :   struct store_byte_from_buffer stored_byte_b;
      11      150000 : 
      12      150000 :   /* There are no loops in the code under test, so use the biggest possible
      13      150000 :    * value */
      14      150000 :   /* Seahorn: initializing both lhs and rhs since init is non det anyways */
      15      150000 : #if defined(__KLEE__) || defined(__FUZZ__)
      16      150000 :   initialize_bounded_aws_hash_table(&a, MAX_TABLE_SIZE);
      17             : #else
      18             :   // There are no loops in the code under test, so use the biggest possible
      19             :   // value
      20             :   initialize_bounded_aws_hash_table(&a, SIZE_MAX);
      21             : #endif
      22      150000 :   assume(aws_hash_table_is_valid(&a));
      23      150000 :   save_byte_from_hash_table(&a, &stored_byte_a);
      24      150000 : 
      25      150000 : #if defined(__KLEE__) || defined(__FUZZ__)
      26      150000 :   initialize_bounded_aws_hash_table(&b, MAX_TABLE_SIZE);
      27             : #else
      28             :   // There are no loops in the code under test, so use the biggest possible
      29             :   // value
      30             :   initialize_bounded_aws_hash_table(&b, SIZE_MAX);
      31             : #endif
      32      150000 :   assume(aws_hash_table_is_valid(&b));
      33      150000 :   save_byte_from_hash_table(&b, &stored_byte_b);
      34      150000 : 
      35      150000 :   aws_hash_table_swap(&a, &b);
      36      150000 : 
      37      150000 :   sassert(aws_hash_table_is_valid(&b));
      38      150000 :   assert_hash_table_unchanged(&b, &stored_byte_a);
      39      150000 :   sassert(aws_hash_table_is_valid(&a));
      40      150000 :   assert_hash_table_unchanged(&a, &stored_byte_b);
      41      150000 :   return 0;
      42      150000 : }