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             : #include <proof_allocators.h>
      10             : 
      11      150000 : int main() {
      12      150000 :     /* data structure */
      13      150000 :     struct aws_byte_buf buf; /* Precondition: buf is non-null */
      14      150000 :     initialize_byte_buf(&buf);
      15      150000 : 
      16      150000 :     /* parameters */
      17      150000 :     struct aws_allocator *allocator = sea_allocator(); /* Precondition: allocator is non-null */
      18      150000 :     size_t capacity = nd_size_t();
      19      150000 :     KLEE_ASSUME(capacity <= KLEE_MAX_SIZE);
      20      150000 : 
      21      150000 :     if (aws_byte_buf_init(&buf, allocator, capacity) == AWS_OP_SUCCESS) {
      22        6347 :         /* assertions */
      23        6347 :         sassert(aws_byte_buf_is_valid(&buf));
      24        6347 :         sassert(buf.allocator == allocator);
      25        6347 :         sassert(buf.len == 0);
      26        6347 :         sassert(buf.capacity == capacity);
      27        6347 :     }
      28      150000 : 
      29      150000 :     return 0;
      30      150000 : }