From c407d3dd8282f2b6c128038f21919113f19da244 Mon Sep 17 00:00:00 2001
From: Nathan Schmidt <nathan.schmidt@tum.de>
Date: Mon, 9 Oct 2023 19:02:55 +0200
Subject: [PATCH] Added test cases to increase coverage

---
 tests/regression/73-strings/05-char_arrays.c | 53 ++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/tests/regression/73-strings/05-char_arrays.c b/tests/regression/73-strings/05-char_arrays.c
index edb5a2ab57..e5c7596063 100644
--- a/tests/regression/73-strings/05-char_arrays.c
+++ b/tests/regression/73-strings/05-char_arrays.c
@@ -20,6 +20,9 @@ int main() {
     example13();
     example14();
     example15();
+    example16();
+    example17();
+    example18();
 
     return 0;
 }
@@ -328,3 +331,53 @@ example15() {
     char* s3 = strstr(s1, s2);
     __goblint_check(s3 == NULL);
 }
+
+example16() {
+    size_t i;
+    if (rand())
+        i = 3;
+    else
+        i = 1/0;
+    
+    char s[5] = "abab";
+    __goblint_check(s[i] != '\0'); // UNKNOWN
+
+    s[4] = 'a';
+    __goblint_check(s[i] != '\0');
+
+    s[4] = '\0';
+    s[i] = '\0';
+    __goblint_check(s[4] == '\0');
+    __goblint_check(s[3] == '\0'); // UNKNOWN
+
+    s[i] = 'a';
+    __goblint_check(s[4] == '\0'); // UNKNOWN
+}
+
+example17() {
+    char s1[20];
+    char s2[10];
+    strcat(s1, s2); // WARN
+    __goblint_check(s1[0] == '\0'); // UNKNOWN
+    __goblint_check(s1[5] == '\0'); // UNKNOWN
+    __goblint_check(s1[12] == '\0'); // UNKNOWN
+}
+
+example18() {
+    char s1[20] = "hello";
+    char s2[10] = "world";
+
+    size_t i;
+    if (rand())
+        i = 1;
+    else
+        i = 2;
+    s1[i] = '\0';
+
+    strcat(s1, s2);
+    __goblint_check(s1[1] != '\0');
+    __goblint_check(s1[6] == '\0'); // UNKNOWN
+    __goblint_check(s1[7] == '\0'); // UNKNOWN
+    __goblint_check(s1[8] != '\0'); // UNKNOWN because might still be uninitialized
+    __goblint_check(s1[10] == '\0'); // UNKNOWN
+}