Initializing local variables to fix undefined behaviors

zvonimir · zvonimir · commit dcb013820149 · 2020-10-23T12:06:45.000-06:00
diff --git a/c/aws-c-common/aws_array_list_back_harness.i b/c/aws-c-common/aws_array_list_back_harness.i
@@ -8014,7 +8014,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 void aws_array_list_back_harness() {
 
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_capacity_harness.i b/c/aws-c-common/aws_array_list_capacity_harness.i
@@ -7991,7 +7991,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_capacity_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_clean_up_harness.i b/c/aws-c-common/aws_array_list_clean_up_harness.i
@@ -7772,7 +7772,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_clean_up_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_clear_harness.i b/c/aws-c-common/aws_array_list_clear_harness.i
@@ -7772,7 +7772,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_clear_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_ensure_capacity_harness.i b/c/aws-c-common/aws_array_list_ensure_capacity_harness.i
@@ -8019,7 +8019,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_ensure_capacity_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_erase_harness.i b/c/aws-c-common/aws_array_list_erase_harness.i
@@ -8069,7 +8069,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_erase_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
     size_t index;
 
 
diff --git a/c/aws-c-common/aws_array_list_front_harness.i b/c/aws-c-common/aws_array_list_front_harness.i
@@ -8011,7 +8011,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_front_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_get_at_harness.i b/c/aws-c-common/aws_array_list_get_at_harness.i
@@ -8013,7 +8013,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_get_at_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_get_at_ptr_harness.i b/c/aws-c-common/aws_array_list_get_at_ptr_harness.i
@@ -8013,7 +8013,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_get_at_ptr_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_init_dynamic_harness.i b/c/aws-c-common/aws_array_list_init_dynamic_harness.i
@@ -7772,7 +7772,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_init_dynamic_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     struct aws_allocator *allocator = can_fail_allocator();
diff --git a/c/aws-c-common/aws_array_list_init_static_harness.i b/c/aws-c-common/aws_array_list_init_static_harness.i
@@ -7602,7 +7602,7 @@ void aws_array_list_swap(struct aws_array_list *restrict list, size_t a, size_t
 }
 void aws_array_list_init_static_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     size_t item_size;
diff --git a/c/aws-c-common/aws_array_list_length_harness.i b/c/aws-c-common/aws_array_list_length_harness.i
@@ -7991,7 +7991,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_length_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_pop_back_harness.i b/c/aws-c-common/aws_array_list_pop_back_harness.i
@@ -8013,7 +8013,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_pop_back_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_pop_front_harness.i b/c/aws-c-common/aws_array_list_pop_front_harness.i
@@ -8009,7 +8009,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_pop_front_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_pop_front_n_harness.i b/c/aws-c-common/aws_array_list_pop_front_n_harness.i
@@ -8009,7 +8009,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_pop_front_n_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
@@ -8022,7 +8022,7 @@ void aws_array_list_pop_front_n_harness() {
     save_byte_from_array((uint8_t *)list.data, list.current_size, &old_byte);
 
 
-    size_t n;
+    size_t n = __VERIFIER_nondet_ulong();
     aws_array_list_pop_front_n(&list, n);
 
 
diff --git a/c/aws-c-common/aws_array_list_push_back_harness.i b/c/aws-c-common/aws_array_list_push_back_harness.i
@@ -8014,7 +8014,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_push_back_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_set_at_harness.i b/c/aws-c-common/aws_array_list_set_at_harness.i
@@ -8014,7 +8014,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_set_at_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_shrink_to_fit_harness.i b/c/aws-c-common/aws_array_list_shrink_to_fit_harness.i
@@ -8055,15 +8055,15 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_shrink_to_fit_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
     ensure_array_list_has_allocated_data_member(&list);
     assume_abort_if_not(aws_array_list_is_valid(&list));
 
 
-    size_t n;
+    size_t n = __VERIFIER_nondet_ulong();
     aws_array_list_pop_front_n(&list, n);
 
 
diff --git a/c/aws-c-common/aws_array_list_sort_harness.i b/c/aws-c-common/aws_array_list_sort_harness.i
@@ -8011,7 +8011,7 @@ int compare(const void *a, const void *b, size_t item_size) {
 
 void aws_array_list_sort_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));
diff --git a/c/aws-c-common/aws_array_list_swap_harness.i b/c/aws-c-common/aws_array_list_swap_harness.i
@@ -8019,7 +8019,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_list_swap_harness() {
 
-    struct aws_array_list list;
+    struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};
 
 
     size_t index_a;

Original file line number	Diff line number	Diff line change
`@@ -7991,7 +7991,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`7991`	`7991`	`}`
`7992`	`7992`	`void aws_array_list_capacity_harness() {`
`7993`	`7993`
`7994`		`- struct aws_array_list list;`
	`7994`	`+ struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};`
`7995`	`7995`
`7996`	`7996`
`7997`	`7997`	`assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));`
Original file line number	Diff line number	Diff line change
`@@ -7772,7 +7772,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`7772`	`7772`	`}`
`7773`	`7773`	`void aws_array_list_clean_up_harness() {`
`7774`	`7774`
`7775`		`- struct aws_array_list list;`
	`7775`	`+ struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};`
`7776`	`7776`
`7777`	`7777`
`7778`	`7778`	`assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));`
Original file line number	Diff line number	Diff line change
`@@ -8019,7 +8019,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`8019`	`8019`	`}`
`8020`	`8020`	`void aws_array_list_ensure_capacity_harness() {`
`8021`	`8021`
`8022`		`- struct aws_array_list list;`
	`8022`	`+ struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};`
`8023`	`8023`
`8024`	`8024`
`8025`	`8025`	`assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));`
Original file line number	Diff line number	Diff line change
`@@ -8069,7 +8069,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`8069`	`8069`	`}`
`8070`	`8070`	`void aws_array_list_erase_harness() {`
`8071`	`8071`
`8072`		`- struct aws_array_list list;`
	`8072`	`+ struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};`
`8073`	`8073`	`size_t index;`
`8074`	`8074`
`8075`	`8075`
Original file line number	Diff line number	Diff line change
`@@ -8011,7 +8011,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`8011`	`8011`	`}`
`8012`	`8012`	`void aws_array_list_front_harness() {`
`8013`	`8013`
`8014`		`- struct aws_array_list list;`
	`8014`	`+ struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};`
`8015`	`8015`
`8016`	`8016`
`8017`	`8017`	`assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));`
Original file line number	Diff line number	Diff line change
`@@ -8013,7 +8013,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`8013`	`8013`	`}`
`8014`	`8014`	`void aws_array_list_get_at_harness() {`
`8015`	`8015`
`8016`		`- struct aws_array_list list;`
	`8016`	`+ struct aws_array_list list = {0, __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), __VERIFIER_nondet_ulong(), 0};`
`8017`	`8017`
`8018`	`8018`
`8019`	`8019`	`assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2));`