LCOV - code coverage report
Current view: top level - seahorn/lib - utils.c (source / functions) Hit Total Coverage
Test: all_fuzz.info Lines: 69 77 89.6 %
Date: 2021-04-23 16:28:21 Functions: 8 10 80.0 %

          Line data    Source code
       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <stdlib.h> // for exit()
       6             : 
       7             : #include <aws/common/private/hash_table_impl.h>
       8             : #include <bounds.h>
       9             : #include <proof_allocators.h>
      10             : #include <seahorn/seahorn.h>
      11             : #include <utils.h>
      12             : 
      13             : void assert_bytes_match(const uint8_t *const a, const uint8_t *const b,
      14     2140836 :                         const size_t len) {
      15     2140836 :   sassert(len == 0 || !a == !b);
      16     2140836 :   if (len > 0 && a != NULL && b != NULL) {
      17     1846975 :     size_t i = nd_size_t();
      18     1846975 :     /* prevent spurious pointer overflows */
      19     1846975 :     assume(i < len && len < MAX_MALLOC);
      20     1846975 :     sassert(a[i] == b[i]);
      21     1846975 :   }
      22     2140836 : }
      23             : 
      24             : void assert_all_bytes_are(const uint8_t *const a, const uint8_t c,
      25      406283 :                           const size_t len) {
      26      406283 :   if (len > 0 && a != NULL) {
      27      405649 :     size_t i = nd_size_t();
      28      405649 :     assume(i < len);
      29      405649 :     sassert(a[i] == c);
      30      405649 :   }
      31      406283 : }
      32             : 
      33      333057 : void assert_all_zeroes(const uint8_t *const a, const size_t len) {
      34      333057 :   assert_all_bytes_are(a, 0, len);
      35      333057 : }
      36             : 
      37             : void assert_byte_from_buffer_matches(
      38      684631 :     const uint8_t *const buffer, const struct store_byte_from_buffer *const b) {
      39      684631 :   if (buffer && b) {
      40      684631 :     sassert(*(buffer + b->index) == b->byte);
      41      684631 :   }
      42      684631 : }
      43             : 
      44             : void save_byte_from_array(const uint8_t *const array, const size_t size,
      45     8124379 :                           struct store_byte_from_buffer *const storage) {
      46     8124379 :   storage->index = nd_size_t();
      47     8124379 :   if (size > 0 && array && storage) {
      48     5521667 :     assume(storage->index < size);
      49     5521667 :     storage->byte = array[storage->index];
      50     5587835 :   } else {
      51     2602712 :     storage->byte = nd_uint8_t();
      52     2602712 :   }
      53     8124379 : }
      54             : 
      55             : void assert_array_list_equivalence(
      56             :     const struct aws_array_list *const lhs,
      57             :     const struct aws_array_list *const rhs,
      58      504080 :     const struct store_byte_from_buffer *const rhs_byte) {
      59      504080 :   /* In order to be equivalent, either both are NULL or both are non-NULL */
      60      504080 :   if (lhs == rhs) {
      61           0 :     return;
      62      504080 :   } else {
      63      504080 :     sassert(lhs && rhs); /* if only one is null, they differ */
      64      504080 :   }
      65      504080 :   sassert(lhs->alloc == rhs->alloc);
      66      504080 :   sassert(lhs->current_size == rhs->current_size);
      67      504080 :   sassert(lhs->length == rhs->length);
      68      504080 :   sassert(lhs->item_size == rhs->item_size);
      69      504080 :   if (lhs->current_size > 0) {
      70      177329 :     assert_byte_from_buffer_matches((uint8_t *)lhs->data, rhs_byte);
      71      177329 :   }
      72      504080 : }
      73             : 
      74             : void assert_byte_buf_equivalence(
      75             :     const struct aws_byte_buf *const lhs, const struct aws_byte_buf *const rhs,
      76      618722 :     const struct store_byte_from_buffer *const rhs_byte) {
      77      618722 :   /* In order to be equivalent, either both are NULL or both are non-NULL */
      78      618722 :   if (lhs == rhs) {
      79           0 :     return;
      80      618722 :   } else {
      81      618722 :     sassert(lhs && rhs); /* if only one is null, they differ */
      82      618722 :   }
      83      618722 :   sassert(lhs->len == rhs->len);
      84      618722 :   sassert(lhs->capacity == rhs->capacity);
      85      618722 :   sassert(lhs->allocator == rhs->allocator);
      86      618722 :   if (lhs->len > 0) {
      87      153396 :     assert_byte_from_buffer_matches(lhs->buffer, rhs_byte);
      88      153396 :   }
      89      618722 : }
      90             : 
      91             : void assert_byte_cursor_equivalence(
      92             :     const struct aws_byte_cursor *const lhs,
      93             :     const struct aws_byte_cursor *const rhs,
      94       24375 :     const struct store_byte_from_buffer *const rhs_byte) {
      95       24375 :   sassert(!lhs == !rhs);
      96       24375 :   if (lhs && rhs) {
      97       24375 :     sassert(lhs->len == rhs->len);
      98       24375 :     if (lhs->len > 0) {
      99        9665 :       assert_byte_from_buffer_matches(lhs->ptr, rhs_byte);
     100        9665 :     }
     101       24375 :   }
     102       24375 : }
     103             : 
     104             : bool uninterpreted_predicate_fn(uint8_t value);
     105             : 
     106           0 : bool nondet_equals(const void *const a, const void *const b) {
     107           0 :   sassert(a != NULL);
     108           0 :   sassert(b != NULL);
     109           0 :   return a == b ? true : nd_bool();
     110           0 : }
     111             : 
     112           0 : uint64_t uninterpreted_hasher(const void *a) { return nd_uint64_t(); }

Generated by: LCOV version 1.13