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 :     /* parameters */
      12      150000 :     struct aws_byte_buf lhs;
      13      150000 :     initialize_byte_buf(&lhs);
      14      150000 :     struct aws_byte_buf rhs;
      15      150000 :     initialize_byte_buf(&rhs);
      16      150000 : 
      17      150000 :     /* assumptions */
      18      150000 :     assume(aws_byte_buf_is_valid(&lhs));
      19      150000 :     if (nd_bool()) {
      20       54285 :         rhs = lhs;
      21       95715 :     } else {
      22       95715 :         assume(aws_byte_buf_is_valid(&rhs));
      23       95715 :     }
      24      150000 : 
      25      150000 :     /* save current state of the data structure */
      26      150000 :     struct aws_byte_buf old_lhs = lhs;
      27      150000 :     struct store_byte_from_buffer old_byte_from_lhs;
      28      150000 :     save_byte_from_array(lhs.buffer, lhs.len, &old_byte_from_lhs);
      29      150000 :     struct aws_byte_buf old_rhs = rhs;
      30      150000 :     struct store_byte_from_buffer old_byte_from_rhs;
      31      150000 :     save_byte_from_array(rhs.buffer, rhs.len, &old_byte_from_rhs);
      32      150000 : 
      33      150000 :     /* operation under verification */
      34      150000 :     if (aws_byte_buf_eq(&lhs, &rhs)) {
      35       29960 :         sassert(lhs.len == rhs.len);
      36       29960 :         if (lhs.len > 0) {
      37       10312 :             assert_bytes_match(lhs.buffer, rhs.buffer, lhs.len);
      38       10312 :         }
      39       29960 :     }
      40      150000 : 
      41      150000 :     /* assertions */
      42      150000 :     sassert(aws_byte_buf_is_valid(&lhs));
      43      150000 :     sassert(aws_byte_buf_is_valid(&rhs));
      44      150000 :     assert_byte_buf_equivalence(&lhs, &old_lhs, &old_byte_from_lhs);
      45      150000 :     assert_byte_buf_equivalence(&rhs, &old_rhs, &old_byte_from_rhs);
      46      150000 : 
      47      150000 :     return 0;
      48      150000 : }