Line data    Source code

       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <aws/common/byte_buf.h>
       6             : #include <byte_buf_helper.h>
       7             : #include <seahorn/seahorn.h>
       8             : #include <utils.h>
       9             : 
      10             : /**
      11             :    SeaHorn does not support inlining of variable number of arguments functions.
      12             :    This is a specialization of aws_byte_buf_cat for 3 arguments.
      13             :  */
      14             : // -- specialize to 3 buffers
      15             : int aws_byte_buf_cat3(struct aws_byte_buf *dest, size_t number_of_args,
      16             :                       struct aws_byte_buf *buf1, struct aws_byte_buf *buf2,
      17       25404 :                       struct aws_byte_buf *buf3) {
      18       25404 :   AWS_PRECONDITION(aws_byte_buf_is_valid(dest));
      19       25404 : 
      20       25404 :   sassert(number_of_args == 3);
      21       25404 :   struct aws_byte_cursor cursor = aws_byte_cursor_from_buf(buf1);
      22       25404 :   if (aws_byte_buf_append(dest, &cursor)) {
      23        2379 :     AWS_POSTCONDITION(aws_byte_buf_is_valid(dest));
      24        2379 :     return AWS_OP_ERR;
      25        2379 :   }
      26       23025 : 
      27       23025 :   cursor = aws_byte_cursor_from_buf(buf2);
      28       23025 :   if (aws_byte_buf_append(dest, &cursor)) {
      29        1789 :     AWS_POSTCONDITION(aws_byte_buf_is_valid(dest));
      30        1789 :     return AWS_OP_ERR;
      31        1789 :   }
      32       21236 : 
      33       21236 :   cursor = aws_byte_cursor_from_buf(buf3);
      34       21236 :   if (aws_byte_buf_append(dest, &cursor)) {
      35        3913 :     AWS_POSTCONDITION(aws_byte_buf_is_valid(dest));
      36        3913 :     return AWS_OP_ERR;
      37        3913 :   }
      38       17323 : 
      39       17323 :   AWS_POSTCONDITION(aws_byte_buf_is_valid(dest));
      40       17323 :   return AWS_OP_SUCCESS;
      41       17323 : }
      42             : 
      43      150000 : int main() {
      44      150000 :   /* parameters */
      45      150000 :   struct aws_byte_buf buffer1;
      46      150000 :   initialize_byte_buf(&buffer1);
      47      150000 :   struct aws_byte_buf buffer2;
      48      150000 :   initialize_byte_buf(&buffer2);
      49      150000 :   struct aws_byte_buf buffer3;
      50      150000 :   initialize_byte_buf(&buffer3);
      51      150000 :   struct aws_byte_buf dest;
      52      150000 :   initialize_byte_buf(&dest);
      53      150000 :   size_t number_of_args = 3;
      54      150000 : 
      55      150000 :   /* assumptions */
      56      150000 :   assume(aws_byte_buf_is_valid(&buffer1));
      57      150000 :   assume(aws_byte_buf_is_valid(&buffer2));
      58      150000 :   assume(aws_byte_buf_is_valid(&buffer3));
      59      150000 :   assume(aws_byte_buf_is_valid(&dest));
      60      150000 : 
      61      150000 :   /* save current state of the data structure */
      62      150000 :   struct aws_byte_buf old_buffer1 = buffer1;
      63      150000 :   struct store_byte_from_buffer old_byte_from_buffer1;
      64      150000 :   save_byte_from_array(buffer1.buffer, buffer1.len, &old_byte_from_buffer1);
      65      150000 :   struct aws_byte_buf old_buffer2 = buffer2;
      66      150000 :   struct store_byte_from_buffer old_byte_from_buffer2;
      67      150000 :   save_byte_from_array(buffer2.buffer, buffer2.len, &old_byte_from_buffer2);
      68      150000 :   struct aws_byte_buf old_buffer3 = buffer3;
      69      150000 :   struct store_byte_from_buffer old_byte_from_buffer3;
      70      150000 :   save_byte_from_array(buffer3.buffer, buffer3.len, &old_byte_from_buffer3);
      71      150000 :   struct aws_byte_buf old_dest = dest;
      72      150000 :   struct store_byte_from_buffer old_byte_from_dest;
      73      150000 :   save_byte_from_array(dest.buffer, dest.len, &old_byte_from_dest);
      74      150000 : 
      75      150000 :   /* operation under verification */
      76      150000 :   if (aws_byte_buf_cat3(&dest, number_of_args, &buffer1, &buffer2, &buffer3) ==
      77      150000 :       AWS_OP_SUCCESS) {
      78       17323 :     sassert((old_dest.capacity - old_dest.len) >=
      79       17323 :             (buffer1.len + buffer2.len + buffer3.len));
      80      132677 :   } else {
      81      132677 :     sassert((old_dest.capacity - old_dest.len) <
      82      132677 :             (buffer1.len + buffer2.len + buffer3.len));
      83      132677 :   }
      84      150000 : 
      85      150000 :   /* assertions */
      86      150000 :   sassert(aws_byte_buf_is_valid(&buffer1));
      87      150000 :   sassert(aws_byte_buf_is_valid(&buffer2));
      88      150000 :   sassert(aws_byte_buf_is_valid(&buffer3));
      89      150000 :   sassert(aws_byte_buf_is_valid(&dest));
      90      150000 :   assert_byte_buf_equivalence(&buffer1, &old_buffer1, &old_byte_from_buffer1);
      91      150000 :   assert_byte_buf_equivalence(&buffer2, &old_buffer2, &old_byte_from_buffer2);
      92      150000 :   assert_byte_buf_equivalence(&buffer3, &old_buffer3, &old_byte_from_buffer3);
      93      150000 : 
      94      150000 :   return 0;
      95      150000 : }