LCOV - code coverage report
Current view: top level - seahorn/jobs/array_list_back - aws_array_list_back_harness.c (source / functions) Hit Total Coverage
Test: all_fuzz.info Lines: 34 34 100.0 %
Date: 2021-04-23 16:28:21 Functions: 1 1 100.0 %

          Line data    Source code
       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <seahorn/seahorn.h>
       6             : #include <aws/common/array_list.h>
       7             : #include <array_list_helper.h>
       8             : #include <utils.h>
       9             : #include <proof_allocators.h>
      10             : 
      11      150000 : int main() {
      12      150000 : 
      13      150000 :     /* data structure */
      14      150000 :     struct aws_array_list list;
      15      150000 :     initialize_bounded_array_list(&list);
      16      150000 : 
      17      150000 :     KLEE_ASSUME(list.item_size != 0);
      18      150000 :     void *val = bounded_malloc(list.item_size);
      19      150000 : 
      20      150000 :     /* assumptions */
      21      150000 :     assume(aws_array_list_is_valid(&list));
      22      150000 : 
      23      150000 :     /* save current state of the data structure */
      24      150000 :     struct aws_array_list old = list;
      25      150000 :     struct store_byte_from_buffer old_byte;
      26      150000 :     save_byte_from_array((uint8_t *)list.data, list.current_size, &old_byte);
      27      150000 : 
      28      150000 :     /* assume preconditions */
      29      150000 :     assume(aws_array_list_is_valid(&list));
      30      150000 :     assume(val && AWS_MEM_IS_WRITABLE(val, list.item_size));
      31      150000 : 
      32      150000 :     /* perform operation under verification */
      33      150000 :     if (aws_array_list_back(&list, val) == AWS_OP_SUCCESS) {
      34       21119 :         /* In the case aws_array_list_back is successful, we can ensure the list isn't empty */
      35       21119 :         sassert(list.data != NULL);
      36       21119 :         sassert(list.length != 0);
      37       21119 :     }
      38      150000 : 
      39      150000 :     /* assertions */
      40      150000 :     sassert(aws_array_list_is_valid(&list));
      41      150000 :     assert_array_list_equivalence(&list, &old, &old_byte);
      42      150000 : 
      43      150000 :     return 0;
      44      150000 : }

Generated by: LCOV version 1.13