Line data    Source code

       1             : #include <aws/common/hash_table.h>
       2             : #include <aws/common/private/hash_table_impl.h>
       3             : #include <config.h>
       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_a;
      10      150000 :   initialize_bounded_aws_hash_table(&map_a, MAX_TABLE_SIZE);
      11      150000 :   map_a.p_impl->equals_fn = nondet_equals;
      12      150000 :   assume(aws_hash_table_is_valid(&map_a));
      13      150000 :   struct store_byte_from_buffer old_byte_a;
      14      150000 :   save_byte_from_hash_table(&map_a, &old_byte_a);
      15      150000 : 
      16      150000 :   struct aws_hash_table map_b;
      17      150000 :   initialize_bounded_aws_hash_table(&map_b, MAX_TABLE_SIZE);
      18      150000 :   map_b.p_impl->equals_fn = nondet_equals;
      19      150000 :   assume(aws_hash_table_is_valid(&map_b));
      20      150000 :   struct store_byte_from_buffer old_byte_b;
      21      150000 :   save_byte_from_hash_table(&map_b, &old_byte_b);
      22      150000 : 
      23      150000 :   bool rval = aws_hash_table_eq(&map_a, &map_b, nondet_equals);
      24      150000 : 
      25      150000 :   sassert(aws_hash_table_is_valid(&map_a));
      26      150000 :   sassert(aws_hash_table_is_valid(&map_b));
      27      150000 :   assert_hash_table_unchanged(&map_a, &old_byte_a);
      28      150000 :   assert_hash_table_unchanged(&map_b, &old_byte_b);
      29      150000 :   return 0;
      30      150000 : }