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 : }
|