Added tests for goto after function.

Author: NlightNFotis

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

@@ -0,0 +1,26 @@
+void param_function(int *old_val, int new_val) 
+{
+    *old_val = new_val;
+}
+
+void param_function_extra(int *old_val, int new_val) 
+{
+    *old_val = new_val;
+}
+
+void test_param_function(int nondet)
+{
+    int a = 5;
+    int b;
+    __CPROVER_assert(a==5,  "a==5");
+    if (nondet) {
+        a = 6;
+        b = 7;
+        goto whatever;
+    }
+    param_function(&a, 10);
+    param_function_extra(&b, 7);
+whatever:
+    __CPROVER_assert(a==10,  "a==10");
+    __CPROVER_assert(b==7, "b==7");
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--function test_param_function --variable --pointers --arrays --structs --verify
+^EXIT=0$
+^SIGNAL=0$
+[test_param_function.assertion.1] .* a==5: Success
+[test_param_function.assertion.2] .* a==10: Unknown
+[test_param_function.assertion.3] .* b==7: Success
+--