Line data    Source code

       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <aws/common/string.h>
       6             : #include <seahorn/seahorn.h>
       7             : #include <byte_buf_helper.h>
       8             : #include <string_helper.h>
       9             : #include <utils.h>
      10             : #include <stddef.h>
      11             : 
      12      150000 : int main() {
      13      150000 :     struct aws_string *str = ensure_string_is_allocated_nondet_length();
      14      150000 :     //struct aws_string *str = ensure_string_is_allocated_bounded_length(SIZE_MAX - 1 - sizeof(struct aws_string));
      15      150000 :     sassert(aws_string_bytes(str) == str->bytes);
      16      150000 :     sassert(aws_string_is_valid(str));
      17      150000 : 
      18      150000 :     return 0;
      19      150000 : }