Line data    Source code

       1             : /**
       2             :  */
       3             : 
       4             : #include <aws/common/hash_table.h>
       5             : #include <aws/common/private/hash_table_impl.h>
       6             : #include <aws/common/string.h>
       7             : 
       8             : #include <seahorn/seahorn.h>
       9             : 
      10             : #include <config.h>
      11             : #include <proof_allocators.h>
      12             : #include <string_helper.h>
      13             : #include <utils.h>
      14             : 
      15           0 : int main(void) {
      16           0 :   size_t len;
      17           0 :   const char *str = ensure_c_str_is_nd_allocated_aligned(MAX_STRING_LEN, &len);
      18           0 : 
      19             :   #ifdef __KLEE__
      20             :     if (!str)
      21             :       return 0;
      22             :   #endif
      23           0 :   assume(aws_c_string_is_valid(str));
      24           0 : 
      25           0 :   uint64_t rval = aws_hash_c_string(str);
      26           0 :   (void)rval;
      27           0 :   return 0;
      28           0 : }