Line data    Source code

       1             : /**
       2             :  */
       3             : 
       4             : #include <aws/common/ring_buffer.h>
       5             : #include <nondet.h>
       6             : #include <seahorn/seahorn.h>
       7             : #include <proof_allocators.h>
       8             : #include <utils.h>
       9             : 
      10      150000 : int main(void) {
      11      150000 :   /* parameters */
      12      150000 :   struct aws_ring_buffer ring_buf;
      13      150000 :   struct aws_allocator *allocator = sea_allocator();
      14      150000 :   size_t size;
      15      150000 :   size = nd_size_t();
      16      150000 :   assume(size > 0); /* Precondition */
      17      150000 :   KLEE_ASSUME(size <= KLEE_MAX_SIZE);
      18      150000 : 
      19      150000 :   if (aws_ring_buffer_init(&ring_buf, allocator, size) == AWS_OP_SUCCESS) {
      20        7919 :     /* assertions */
      21        7919 :     sassert(aws_ring_buffer_is_valid(&ring_buf));
      22        7919 :     sassert(ring_buf.allocator == allocator);
      23        7919 :     sassert(ring_buf.allocation_end - ring_buf.allocation == size);
      24        7919 :   }
      25      150000 :   return 0;
      26      150000 : }