Line data    Source code

       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <aws/common/byte_buf.h>
       6             : #include <byte_buf_helper.h>
       7             : #include <string_helper.h>
       8             : #include <proof_allocators.h>
       9             : #include <seahorn/seahorn.h>
      10             : #include <utils.h>
      11             : 
      12      150000 : int main() {
      13      150000 :     /* parameter */
      14      150000 :     size_t str_len;
      15      150000 :     const char *c_str = ensure_c_str_is_nd_allocated(MAX_BUFFER_SIZE, &str_len);
      16      150000 : 
      17      150000 :     /* operation under verification */
      18      150000 :     struct aws_byte_cursor cur = aws_byte_cursor_from_c_str(c_str);
      19      150000 : 
      20      150000 :     /* assertions */
      21      150000 :     sassert(aws_byte_cursor_is_valid(&cur));
      22      150000 :     if (cur.ptr) { /* if ptr is NULL len shoud be 0, otherwise equal to c_str */
      23      125331 :         sassert(cur.len == str_len);
      24      125331 :         assert_bytes_match(cur.ptr, (uint8_t *)c_str, cur.len);
      25      125331 :     } else {
      26       24669 :         sassert(cur.len == 0);
      27       24669 :     }
      28      150000 : 
      29      150000 :     return 0;
      30      150000 : }