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 :     /* parameters */
      12      150000 :     struct aws_byte_buf buf;
      13      150000 :     initialize_byte_buf(&buf);
      14      150000 :     struct aws_byte_buf output;
      15      150000 :     size_t len = nd_size_t();
      16      150000 : 
      17      150000 :     /* assumptions */
      18      150000 :     assume(aws_byte_buf_is_valid(&buf));
      19      150000 :     if (nd_bool()) {
      20       59114 :         output = buf;
      21       90886 :     } else {
      22       90886 :         initialize_byte_buf(&output);
      23       90886 :         assume(aws_byte_buf_is_valid(&output));
      24       90886 :     }
      25      150000 : 
      26      150000 :     /* save current state of the parameters */
      27      150000 :     struct aws_byte_buf old = buf;
      28      150000 :     struct store_byte_from_buffer old_byte_from_buf;
      29      150000 :     save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf);
      30      150000 : 
      31      150000 :     /* operation under verification */
      32      150000 :     if (aws_byte_buf_advance(&buf, &output, len)) {
      33        7265 :         sassert(buf.len == old.len + len);
      34        7265 :         sassert(buf.capacity == old.capacity);
      35        7265 :         sassert(buf.allocator == old.allocator);
      36        7265 :         if (old.len > 0) {
      37        3554 :             assert_byte_from_buffer_matches(buf.buffer, &old_byte_from_buf);
      38        3554 :         }
      39        7265 :         sassert(output.len == 0);
      40        7265 :         sassert(output.capacity == len);
      41        7265 :         sassert(output.allocator == NULL);
      42      142735 :     } else {
      43      142735 :         assert_byte_buf_equivalence(&buf, &old, &old_byte_from_buf);
      44      142735 :         sassert(output.len == 0);
      45      142735 :         sassert(output.capacity == 0);
      46      142735 :         sassert(output.allocator == NULL);
      47      142735 :         sassert(output.buffer == NULL);
      48      142735 :     }
      49      150000 :     sassert(aws_byte_buf_is_valid(&buf));
      50      150000 :     sassert(aws_byte_buf_is_valid(&output));
      51      150000 : 
      52      150000 :     return 0;
      53      150000 : }