Line data    Source code

       1             : #include <seahorn/seahorn.h>
       2             : #include <aws/common/hash_table.h>
       3             : #include <nondet.h>
       4             : 
       5      150000 : int main(void) {
       6      150000 :     /* hash value of ptr itself only, so deref should be illegal */
       7      150000 :     void *ptr = nd_voidp();
       8      150000 :     /* This function has no pre or post conditions */
       9      150000 :     /* passively checks mem safety */
      10      150000 :     uint64_t rval = aws_hash_ptr(ptr);
      11      150000 :     return 0;
      12      150000 : }