Line data    Source code

       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <aws/common/string.h>
       6             : #include <byte_buf_helper.h>
       7             : #include <seahorn/seahorn.h>
       8             : #include <stddef.h>
       9             : #include <string_helper.h>
      10             : #include <utils.h>
      11             : 
      12      150000 : int main(void) {
      13      150000 :   struct aws_string *str =
      14      150000 :       nd_bool() ? ensure_string_is_allocated_nondet_length() : NULL;
      15      150000 :   aws_string_destroy(str);
      16      150000 : 
      17      150000 :   return 0;
      18      150000 : }