Line data    Source code

       1             : /*
       2             :  * 
       3             :  */
       4             : 
       5             : #include <seahorn/seahorn.h>
       6             : #include <aws/common/byte_buf.h>
       7             : #include <byte_buf_helper.h>
       8             : #include <utils.h>
       9             : 
      10      150000 : int main() {
      11      150000 :     struct aws_byte_buf to;
      12      150000 :     initialize_byte_buf(&to);
      13      150000 :     assume(aws_byte_buf_is_valid(&to));
      14      150000 : 
      15      150000 :     /* save current state of the data structure */
      16      150000 :     struct aws_byte_buf to_old = to;
      17      150000 : 
      18      150000 :     struct aws_byte_cursor from;
      19      150000 :     initialize_byte_cursor(&from);
      20      150000 :     assume(aws_byte_cursor_is_valid(&from));
      21      150000 : 
      22      150000 :     /* save current state of the data structure */
      23      150000 :     struct aws_byte_cursor from_old = from;
      24      150000 : 
      25      150000 :     if (aws_byte_buf_append(&to, &from) == AWS_OP_SUCCESS) {
      26       51284 :         sassert(to.len == to_old.len + from.len);
      27       98716 :     } else {
      28       98716 :         /* if the operation return an error, to must not change */
      29       98716 :         assert_bytes_match(to_old.buffer, to.buffer, to.len);
      30       98716 :         sassert(to_old.len == to.len);
      31       98716 :     }
      32      150000 : 
      33      150000 :     sassert(aws_byte_buf_is_valid(&to));
      34      150000 :     sassert(aws_byte_cursor_is_valid(&from));
      35      150000 :     sassert(to_old.allocator == to.allocator);
      36      150000 :     sassert(to_old.capacity == to.capacity);
      37      150000 :     assert_bytes_match(from_old.ptr, from.ptr, from.len);
      38      150000 :     sassert(from_old.len == from.len);
      39      150000 : 
      40      150000 :     return 0;
      41      150000 : }