Merge pull request sosy-lab#1253 from sosy-lab/aws-variable-initializ…

…ation Properly initialize local variables in c/aws-c-common/mem*.i
tautschnig · Dec 3, 2020 · efea738 · efea738
2 parents 5f7451b + 287def7
commit efea738
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 5 deletions.
diff --git a/c/aws-c-common/memcpy_using_uint64_harness.i b/c/aws-c-common/memcpy_using_uint64_harness.i
@@ -218,6 +218,7 @@ extern short __VERIFIER_nondet_short();
 extern unsigned int __VERIFIER_nondet_uint();
 extern unsigned long __VERIFIER_nondet_ulong();
 extern unsigned char __VERIFIER_nondet_uchar();
+extern char __VERIFIER_nondet_char();
 
 void __VERIFIER_assert(_Bool cond) {
     if(!cond) {reach_error();abort();}
@@ -5930,8 +5931,11 @@ void memcpy_using_uint64_harness() {
     char s[160];
     char d1[160];
     char d2[160];
+    for (int i = 0; i < 160; i++) {
+        s[i] = __VERIFIER_nondet_char();
+    }
 
-    unsigned size;
+    unsigned size = __VERIFIER_nondet_uint();
     assume_abort_if_not(size < 160);
     memcpy_impl(d1, s, size);
     memcpy_using_uint64_impl(d2, s, size);

diff --git a/c/aws-c-common/memset_override_0_harness.i b/c/aws-c-common/memset_override_0_harness.i
@@ -5905,10 +5905,10 @@ void memset_override_0_harness() {
 
     short d1[160];
     short d2[160];
-    int c;
+    int c = __VERIFIER_nondet_int();
     assume_abort_if_not(c == 0);
 
-    unsigned size;
+    unsigned size = __VERIFIER_nondet_uint();;
     assume_abort_if_not((size & 0x7) == 0);
     assume_abort_if_not(size < 160);
     memset_impl(d1, c, size);

diff --git a/c/aws-c-common/memset_using_uint64_harness.i b/c/aws-c-common/memset_using_uint64_harness.i
@@ -5936,8 +5936,8 @@ void memset_using_uint64_harness() {
 
     short d1[160];
     short d2[160];
-    int c;
-    unsigned size;
+    int c = __VERIFIER_nondet_int();
+    unsigned size = __VERIFIER_nondet_uint();
     assume_abort_if_not(size < 160);
     memset_impl(d1, c, size);
     memset_using_uint64_impl(d2, c, size);