Fixing more undef behaviors

zvonimir · zvonimir · commit 131eb496833f · 2020-10-24T15:17:33.000-06:00
diff --git a/c/aws-c-common/aws_array_eq_c_str_harness.i b/c/aws-c-common/aws_array_eq_c_str_harness.i
@@ -9112,7 +9112,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 void aws_array_eq_c_str_harness() {
 
     void *array;
-    size_t array_len;
+    size_t array_len = __VERIFIER_nondet_ulong();
     assume_abort_if_not(array_len <= 10);
     array = can_fail_malloc(array_len);
     const char *c_str = nondet_bool() ? 
diff --git a/c/aws-c-common/aws_array_eq_c_str_ignore_case_harness.i b/c/aws-c-common/aws_array_eq_c_str_ignore_case_harness.i
@@ -9111,7 +9111,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_eq_c_str_ignore_case_harness() {
 
-    size_t array_len;
+    size_t array_len = __VERIFIER_nondet_ulong();
     assume_abort_if_not(array_len <= 10);
     void *array = can_fail_malloc(array_len);
     const char *c_str = nondet_bool() ? 
diff --git a/c/aws-c-common/aws_array_eq_harness.i b/c/aws-c-common/aws_array_eq_harness.i
@@ -9111,12 +9111,12 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_eq_harness() {
 
-    size_t lhs_len;
+    size_t lhs_len = __VERIFIER_nondet_ulong();
     assume_abort_if_not(lhs_len <= 10);
     void *lhs = can_fail_malloc(lhs_len);
 
     void *rhs;
-    size_t rhs_len;
+    size_t rhs_len = __VERIFIER_nondet_ulong();
     if (nondet_bool()) {
         rhs_len = lhs_len;
         rhs = lhs;
diff --git a/c/aws-c-common/aws_array_eq_ignore_case_harness.i b/c/aws-c-common/aws_array_eq_ignore_case_harness.i
@@ -9111,12 +9111,12 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_array_eq_ignore_case_harness() {
 
-    size_t lhs_len;
+    size_t lhs_len = __VERIFIER_nondet_ulong();
     assume_abort_if_not(lhs_len <= 10);
     void *lhs = can_fail_malloc(lhs_len);
 
     void *rhs;
-    size_t rhs_len;
+    size_t rhs_len = __VERIFIER_nondet_ulong();
     if (nondet_bool()) {
         rhs_len = lhs_len;
         rhs = lhs;
diff --git a/c/aws-c-common/aws_array_list_comparator_string_harness.i b/c/aws-c-common/aws_array_list_comparator_string_harness.i
@@ -9881,10 +9881,10 @@ void aws_array_list_comparator_string_harness() {
     struct aws_string *str_b = nondet_bool() ? str_a : ensure_string_is_allocated_bounded_length(16);
     
    _Bool 
-        nondet_parameter_a;
+        nondet_parameter_a = nondet_bool();
     
    _Bool 
-        nondet_parameter_b;
+        nondet_parameter_b = nondet_bool();
     if (aws_array_list_comparator_string(nondet_parameter_a ? &str_a : 
                                                                       ((void *)0)
                                                                           , nondet_parameter_b ? &str_b : 
diff --git a/c/aws-c-common/aws_byte_buf_advance_harness.i b/c/aws-c-common/aws_byte_buf_advance_harness.i
@@ -9112,9 +9112,9 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_buf_advance_harness() {
 
-    struct aws_byte_buf buf;
-    struct aws_byte_buf output;
-    size_t len;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
+    struct aws_byte_buf output = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
+    size_t len = __VERIFIER_nondet_ulong();
 
 
     assume_abort_if_not(aws_byte_buf_is_bounded(&buf, 40));
diff --git a/c/aws-c-common/aws_byte_buf_cat_harness.i b/c/aws-c-common/aws_byte_buf_cat_harness.i
@@ -9111,10 +9111,10 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_buf_cat_harness() {
 
-    struct aws_byte_buf buffer1;
-    struct aws_byte_buf buffer2;
-    struct aws_byte_buf buffer3;
-    struct aws_byte_buf dest;
+    struct aws_byte_buf buffer1 = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
+    struct aws_byte_buf buffer2 = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
+    struct aws_byte_buf buffer3 = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
+    struct aws_byte_buf dest = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
     size_t number_of_args = 3;
 
 
diff --git a/c/aws-c-common/aws_byte_buf_eq_c_str_harness.i b/c/aws-c-common/aws_byte_buf_eq_c_str_harness.i
@@ -9111,7 +9111,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_buf_eq_c_str_harness() {
 
-    struct aws_byte_buf buf;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
     const char *c_str = ensure_c_str_is_allocated(10);
 
 
diff --git a/c/aws-c-common/aws_byte_buf_eq_c_str_ignore_case_harness.i b/c/aws-c-common/aws_byte_buf_eq_c_str_ignore_case_harness.i
@@ -9111,7 +9111,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_buf_eq_c_str_ignore_case_harness() {
 
-    struct aws_byte_buf buf;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
     const char *c_str = ensure_c_str_is_allocated(10);
 
 
diff --git a/c/aws-c-common/aws_byte_buf_write_from_whole_string_harness.i b/c/aws-c-common/aws_byte_buf_write_from_whole_string_harness.i
@@ -9880,7 +9880,7 @@ void aws_byte_buf_write_from_whole_string_harness() {
     struct aws_string *str = nondet_bool() ? ensure_string_is_allocated_bounded_length(16) : 
                                                                                                         ((void *)0)
                                                                                                             ;
-    struct aws_byte_buf buf;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
 
     ensure_byte_buf_has_allocated_buffer_member(&buf);
     assume_abort_if_not(aws_byte_buf_is_valid(&buf));
diff --git a/c/aws-c-common/aws_byte_buf_write_harness.i b/c/aws-c-common/aws_byte_buf_write_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_buf_write_harness() {
 
-    struct aws_byte_buf buf;
-    size_t len;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
+    size_t len = __VERIFIER_nondet_ulong();
     uint8_t *array = bounded_malloc(len);
 
 
diff --git a/c/aws-c-common/aws_byte_cursor_advance_harness.i b/c/aws-c-common/aws_byte_cursor_advance_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_advance_harness() {
 
-    struct aws_byte_cursor cursor;
-    size_t len;
+    struct aws_byte_cursor cursor = {__VERIFIER_nondet_ulong(), 0};
+    size_t len = __VERIFIER_nondet_ulong();
 
 
     ensure_byte_cursor_has_allocated_buffer_member(&cursor);
diff --git a/c/aws-c-common/aws_byte_cursor_advance_nospec_harness.i b/c/aws-c-common/aws_byte_cursor_advance_nospec_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_advance_nospec_harness() {
 
-    struct aws_byte_cursor cursor;
-    size_t len;
+    struct aws_byte_cursor cursor = {__VERIFIER_nondet_ulong(), 0};
+    size_t len = __VERIFIER_nondet_ulong();
 
 
     ensure_byte_cursor_has_allocated_buffer_member(&cursor);
diff --git a/c/aws-c-common/aws_byte_cursor_from_buf_harness.i b/c/aws-c-common/aws_byte_cursor_from_buf_harness.i
@@ -9090,7 +9090,7 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_from_buf_harness() {
 
-    struct aws_byte_buf buf;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
 
 
     assume_abort_if_not(aws_byte_buf_is_bounded(&buf, 10));
diff --git a/c/aws-c-common/aws_byte_cursor_read_and_fill_buffer_harness.i b/c/aws-c-common/aws_byte_cursor_read_and_fill_buffer_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_read_and_fill_buffer_harness() {
 
-    struct aws_byte_cursor cur;
-    struct aws_byte_buf buf;
+    struct aws_byte_cursor cur = {__VERIFIER_nondet_ulong(), 0};
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
 
 
     ensure_byte_cursor_has_allocated_buffer_member(&cur);
diff --git a/c/aws-c-common/aws_byte_cursor_read_be16_harness.i b/c/aws-c-common/aws_byte_cursor_read_be16_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_read_common_harness() {
 
-    struct aws_byte_cursor cur;
-    size_t length;
+    struct aws_byte_cursor cur = {__VERIFIER_nondet_ulong(), 0};
+    size_t length = __VERIFIER_nondet_ulong();
     uint16_t *dest = can_fail_malloc(length);
 
 
diff --git a/c/aws-c-common/aws_byte_cursor_read_be32_harness.i b/c/aws-c-common/aws_byte_cursor_read_be32_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_read_common_harness() {
 
-    struct aws_byte_cursor cur;
-    size_t length;
+    struct aws_byte_cursor cur = {__VERIFIER_nondet_ulong(), 0};
+    size_t length = __VERIFIER_nondet_ulong();
     uint32_t *dest = can_fail_malloc(length);
 
 
diff --git a/c/aws-c-common/aws_byte_cursor_read_be64_harness.i b/c/aws-c-common/aws_byte_cursor_read_be64_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_read_common_harness() {
 
-    struct aws_byte_cursor cur;
-    size_t length;
+    struct aws_byte_cursor cur = {__VERIFIER_nondet_ulong(), 0};
+    size_t length = __VERIFIER_nondet_ulong();
     uint64_t *dest = can_fail_malloc(length);
 
 
diff --git a/c/aws-c-common/aws_byte_cursor_read_harness.i b/c/aws-c-common/aws_byte_cursor_read_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_read_harness() {
 
-    struct aws_byte_cursor cur;
-    size_t length;
+    struct aws_byte_cursor cur = {__VERIFIER_nondet_ulong(), 0};
+    size_t length = __VERIFIER_nondet_ulong();
     void *dest = bounded_malloc(length);
 
 
diff --git a/c/aws-c-common/aws_byte_cursor_read_u8_harness.i b/c/aws-c-common/aws_byte_cursor_read_u8_harness.i
@@ -9090,8 +9090,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_byte_cursor_read_u8_harness() {
 
-    struct aws_byte_cursor cur;
-    size_t length;
+    struct aws_byte_cursor cur = {__VERIFIER_nondet_ulong(), 0};
+    size_t length = __VERIFIER_nondet_ulong();
     uint8_t *dest = bounded_malloc(length);
 
 
diff --git a/c/aws-c-common/aws_is_power_of_two_harness.i b/c/aws-c-common/aws_is_power_of_two_harness.i
@@ -2665,7 +2665,7 @@ static inline int aws_round_up_to_power_of_two(size_t n, size_t *result) {
 
 
 void aws_is_power_of_two_harness() {
-    size_t test_val;
+    size_t test_val = __VERIFIER_nondet_ulong();
     
    _Bool 
         rval = aws_is_power_of_two(test_val);
diff --git a/c/aws-c-common/aws_nospec_mask_harness.i b/c/aws-c-common/aws_nospec_mask_harness.i
@@ -8871,8 +8871,8 @@ void aws_common_fatal_assert_library_initialized(void) {
 }
 void aws_nospec_mask_harness() {
 
-    size_t index;
-    size_t bound;
+    size_t index = __VERIFIER_nondet_ulong();
+    size_t bound = __VERIFIER_nondet_ulong();
 
 
     size_t rval = aws_nospec_mask(index, bound);
diff --git a/c/aws-c-common/aws_round_up_to_power_of_two_harness.i b/c/aws-c-common/aws_round_up_to_power_of_two_harness.i
@@ -2682,8 +2682,8 @@ static inline int aws_round_up_to_power_of_two(size_t n, size_t *result) {
 
 
 void aws_round_up_to_power_of_two_harness() {
-    size_t test_val;
-    size_t result;
+    size_t test_val = __VERIFIER_nondet_ulong();
+    size_t result = __VERIFIER_nondet_ulong();
     int rval = aws_round_up_to_power_of_two(test_val, &result);
 
 
diff --git a/c/aws-c-common/aws_string_eq_byte_buf_harness.i b/c/aws-c-common/aws_string_eq_byte_buf_harness.i
@@ -9671,7 +9671,7 @@ void aws_string_eq_byte_buf_harness() {
     struct aws_string *str = nondet_bool() ? ensure_string_is_allocated_bounded_length(16) : 
                                                                                                         ((void *)0)
                                                                                                             ;
-    struct aws_byte_buf buf;
+    struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};
 
     assume_abort_if_not(aws_byte_buf_is_bounded(&buf, 16));
     ensure_byte_buf_has_allocated_buffer_member(&buf);
diff --git a/c/aws-c-common/aws_string_eq_byte_cursor_harness.i b/c/aws-c-common/aws_string_eq_byte_cursor_harness.i
@@ -9670,14 +9670,14 @@ void aws_string_eq_byte_cursor_harness() {
     struct aws_string *str = nondet_bool() ? ensure_string_is_allocated_bounded_length(16) : 
                                                                                                         ((void *)0)
                                                                                                             ;
-    struct aws_byte_cursor cursor;
+    struct aws_byte_cursor cursor = {__VERIFIER_nondet_ulong(), 0};
 
     ensure_byte_cursor_has_allocated_buffer_member(&cursor);
     assume_abort_if_not(aws_byte_cursor_is_valid(&cursor));
 
     
    _Bool 
-        nondet_parameter;
+        nondet_parameter = nondet_bool();
     if (aws_string_eq_byte_cursor(str, nondet_parameter ? &cursor : 
                                                                    ((void *)0)
                                                                        ) && str) {

Original file line number	Diff line number	Diff line change
`@@ -9111,7 +9111,7 @@ void aws_common_fatal_assert_library_initialized(void) {`
`9111`	`9111`	`}`
`9112`	`9112`	`void aws_array_eq_c_str_ignore_case_harness() {`
`9113`	`9113`
`9114`		`- size_t array_len;`
	`9114`	`+ size_t array_len = __VERIFIER_nondet_ulong();`
`9115`	`9115`	`assume_abort_if_not(array_len <= 10);`
`9116`	`9116`	`void *array = can_fail_malloc(array_len);`
`9117`	`9117`	`const char *c_str = nondet_bool() ?`
Original file line number	Diff line number	Diff line change
`@@ -9880,7 +9880,7 @@ void aws_byte_buf_write_from_whole_string_harness() {`
`9880`	`9880`	`struct aws_string *str = nondet_bool() ? ensure_string_is_allocated_bounded_length(16) :`
`9881`	`9881`	`((void *)0)`
`9882`	`9882`	`;`
`9883`		`- struct aws_byte_buf buf;`
	`9883`	`+ struct aws_byte_buf buf = {__VERIFIER_nondet_ulong(), 0, __VERIFIER_nondet_ulong(), 0};`
`9884`	`9884`
`9885`	`9885`	`ensure_byte_buf_has_allocated_buffer_member(&buf);`
`9886`	`9886`	`assume_abort_if_not(aws_byte_buf_is_valid(&buf));`