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             : /**
      12             :  * Runtime: 7s
      13             :  */
      14      150000 : int main() {
      15      150000 :     /* data structure */
      16      150000 :     struct aws_array_list list;
      17      150000 :     initialize_bounded_array_list(&list);
      18      150000 : 
      19      150000 :     /* assumptions */
      20      150000 :     assume(aws_array_list_is_valid(&list));
      21      150000 : 
      22      150000 :     /* save current state of the data structure */
      23      150000 :     struct aws_array_list old = list;
      24      150000 :     struct store_byte_from_buffer old_byte;
      25      150000 :     save_byte_from_array((uint8_t *)list.data, list.current_size, &old_byte);
      26      150000 : 
      27      150000 :     /* perform operation under verification */
      28      150000 :     size_t len = aws_array_list_length(&list);
      29      150000 : 
      30      150000 :     /* assertions */
      31      150000 :     sassert(aws_array_list_is_valid(&list));
      32      150000 :     assert_array_list_equivalence(&list, &old, &old_byte);
      33      150000 : 
      34      150000 :     return 0;
      35      150000 : }