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 buf;
      12      150000 :     initialize_byte_buf(&buf);
      13      150000 :     
      14      150000 :     assume(aws_byte_buf_is_valid(&buf));
      15      150000 : 
      16      150000 :     //struct aws_byte_buf old = buf;
      17      150000 :     size_t requested_capacity = nd_size_t();
      18             :     #ifdef __KLEE__
      19             :         if (requested_capacity > MAX_BUFFER_SIZE) return 0;
      20             :         if (buf.capacity >= MAX_BUFFER_SIZE) return 0;
      21             :     #else 
      22      150000 :         assume(requested_capacity <= MAX_BUFFER_SIZE);
      23      150000 :         assume(buf.capacity < MAX_BUFFER_SIZE);
      24      150000 :     #endif
      25      150000 : 
      26      150000 :     if (aws_byte_buf_reserve(&buf, requested_capacity) == AWS_OP_SUCCESS) {
      27       13200 :         sassert(buf.capacity >= requested_capacity);
      28       13200 :         //sassert(aws_byte_buf_has_allocator(&buf));
      29       13200 :     }
      30      150000 : 
      31      150000 :     /*sassert(aws_byte_buf_is_valid(&buf));
      32      150000 :     sassert(old.len == buf.len);
      33      150000 :     sassert(old.allocator == buf.allocator);
      34      150000 :     if (!buf.buffer) {
      35      150000 :         assert_bytes_match(old.buffer, buf.buffer, buf.len);
      36      150000 :     }*/
      37      150000 : 
      38      150000 :     return 0;
      39      150000 : }