Added tests for the non-terminating function case.

Author: NlightNFotis

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-non-terminating-function/main.c

@@ -0,0 +1,32 @@
+int non_terminating(int *a, int val)
+{
+    while (1)
+    {
+        a = val;
+    }
+    return a;
+}
+
+int non_terminating_extra(int *a, int val)
+{
+    while (1)
+    {
+        a = val;
+    }
+    return a;
+}
+
+void test_non_terminating()
+{
+    int one_val = 5;
+    int second_val = 6;
+    __CPROVER_assert(one_val==5,  "one_val==5");
+    __CPROVER_assert(second_val==6,  "second_val==6");
+
+    non_terminating(&one_val, 10);
+    __CPROVER_assert(one_val==10,  "one_val==10");
+    non_terminating_extra(&second_val, 12);
+    __CPROVER_assert(second_val==12,  "second_val==12");
+    non_terminating_extra(&second_val, 13);
+    __CPROVER_assert(second_val==13,  "second_val==13");
+}

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-non-terminating-function/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--function test_non_terminating --variable --pointers --arrays --structs --verify
+^EXIT=0$
+^SIGNAL=0$
+[test_non_terminating.assertion.1] .* one_val==5: Success
+[test_non_terminating.assertion.2] .* second_val==6: Success
+[test_non_terminating.assertion.3] .* one_val==10: Success \(unreachable\)
+[test_non_terminating.assertion.4] .* second_val==12: Success \(unreachable\)
+[test_non_terminating.assertion.5] .* second_val==13: Success \(unreachable\)
+--