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_a = nd_bool() ?
      14      136983 :             ensure_string_is_allocated_bounded_length(MAX_BUFFER_SIZE) :
      15      150000 :             NULL;
      16      150000 :     struct aws_string *str_b = nd_bool() ?
      17       55686 :             (nd_bool() ? str_a : NULL) :
      18      150000 :             ensure_string_is_allocated_bounded_length(MAX_BUFFER_SIZE);
      19      150000 :     bool nondet_parameter = nd_bool();
      20      150000 :     if (aws_string_compare(str_a, nondet_parameter ? str_b : str_a) == AWS_OP_SUCCESS) {
      21       84625 :         if (nondet_parameter && str_a && str_b) {
      22       36687 :             assert_bytes_match(str_a->bytes, str_b->bytes, str_a->len);
      23       36687 :         }
      24       84625 :     }
      25      150000 :     if (str_a) {
      26       81476 :         sassert(aws_string_is_valid(str_a));
      27       81476 :     }
      28      150000 :     if (str_b) {
      29       79514 :         sassert(aws_string_is_valid(str_b));
      30       79514 :     }
      31      150000 : 
      32      150000 :     return 0;
      33      150000 : }