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 :     bool zero_contents = nd_bool();
      18      150000 :     aws_byte_buf_reset(&buf, zero_contents);
      19      150000 :     sassert(buf.len == 0);
      20      150000 :     sassert(buf.allocator == old.allocator);
      21      150000 :     sassert(buf.buffer == old.buffer);
      22      150000 :     sassert(buf.capacity == old.capacity);
      23      150000 :     if (zero_contents) {
      24       73226 :         assert_all_bytes_are(buf.buffer, 0, buf.capacity);
      25       73226 :     }
      26      150000 : 
      27      150000 :     return 0;
      28      150000 : }