updated testcases loopfreeCallstring + callstring fundec

src/framework/constraints.ml

@@ -568,8 +568,8 @@ struct
   let asm ctx                                     = S.asm (conv ctx), cg_val ctx
   let skip ctx                                    = S.skip (conv ctx), cg_val ctx
   let special ctx r f args                        = S.special (conv ctx) r f args, cg_val ctx
-  let combine_env ctx r fe f args fc es f_ask     = S.combine_env (conv ctx) r fe f args (Option.bind fc (fun x -> x)) (fst es) f_ask, cg_val ctx
-  let combine_assign ctx r fe f args fc es f_ask  = S.combine_assign (conv ctx) r fe f args (Option.bind fc (fun x -> x)) (fst es) f_ask, cg_val ctx
+  let combine_env ctx r fe f args fc es f_ask     = S.combine_env (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
+  let combine_assign ctx r fe f args fc es f_ask  = S.combine_assign (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
   let paths_as_set ctx                            = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx) 
   let threadspawn ctx ~multiple lval f args fctx  = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx
   let event ctx e octx                            = S.event (conv ctx) e (conv octx), cg_val ctx

tests/regression/81-loopfree_callstring/01-loop_calling_sens.c

@@ -19,7 +19,7 @@ int f(int i)
 int main()
 {
     // main -> f(7) -> g(6) -> f(5) -> ... -> f(1) -> g(0) -> return 2
-    // [main, f, g] and [main] {f, g}
+    // [main, f, g] and [main] {f, g} (3 times)
     __goblint_check(f(7) == 2);
     return 0;
 }

tests/regression/81-loopfree_callstring/02-loop_calling_ins.c

@@ -25,6 +25,6 @@ int f(int i)
 int main(void)
 {
     // main -> f(9) -> g(8) -> f(7) -> ... -> g(2) -> f(1) -> g(0) -> return 2
-    // [main, f, g] and [main] {f, g}
+    // [main, f, g] and [main] {f, g} (4 times)
     __goblint_check(f(9) == 2); // UNKNOWN
 }

tests/regression/81-loopfree_callstring/06-multiple_calls_sens.c

@@ -44,7 +44,7 @@ int h(int i)
 int main(void)
 {
     // main -> f(3) -> ... -> f(0) -> return 11
-    // [main, f] and [main] {f}
+    // [main, f] and [main] {f} (3 times)
     __goblint_check(f(3) == 11);
 
     // main -> g(3) -> f(2) -> f(1) -> f(0) -> return 11

tests/regression/81-loopfree_callstring/07-multiple_calls_ins.c

@@ -44,14 +44,14 @@ int h(int i)
 int main(void)
 {
     // main -> f(4) -> f(3) -> f(2) -> f(1) -> f(0) -> return 11
-    // [main, f] and [main] {f}
+    // [main, f] and [main] {f} (4 times)
     __goblint_check(f(4) == 11); // UNKNOWN
 
     // main -> g(20) -> f(19) -> ... -> f(0) -> return 11
-    // [main, g, f] and [main, g] {f}
+    // [main, g, f] and [main, g] {f} (20 times)
     __goblint_check(g(20) == 11); // UNKNOWN
 
     // main -> h(10) -> g(9) -> f(8) -> ... -> f(1) -> f(0) -> return 11
-    // [main, h, g, f] and [main, h, g] {f}
+    // [main, h, g, f] and [main, h, g] {f} (9 times)
     __goblint_check(h(10) == 11); // UNKNOWN
 }

tests/regression/81-loopfree_callstring/08-new_calling_set.c

@@ -31,6 +31,6 @@ int g(int i)
 int main(void)
 {
     // main -> g(20) -> ... -> g(5) -> f(4) -> ... -> f(0) -> return 1
-    // [main] {g, f}
+    // [main] {g} (16 times) and [main] {g, f} (5 times)
     __goblint_check(g(20) == 1); // UNKNOWN
 }

tests/regression/81-loopfree_callstring/09-many_nested_loops.c

@@ -67,12 +67,12 @@ int main(void)
     // m:       [main, m]
     // g:       [main, m, g]
     // f:       [main, m, g, f]
-    // f:       [main, m, g] {f}
+    // f:       [main, m, g] {f} (3 times)
     // h:       [main, m, g] {f} [h]
     // g:       [main, m] {g, f, h}
     // a:       [main, m] {g, f, h} [a]
     // b:       [main, m] {g, f, h} [a, b]
     // c:       [main, m] {g, f, h} [a, b, c]
-    // g, b, c: [main, m] {g, f, h, a, b, c}
+    // g, b, c: [main, m] {g, f, h, a, b, c} (3 times)
     __goblint_check(m(4) == 4);
 }

tests/regression/81-loopfree_callstring/10-nested_loops.c

@@ -27,6 +27,6 @@ int f(int i)
 int main(void)
 {
     // main -> f(4) -> f(3) -> ... -> f(0) -> g(2) -> h(2) -> return 3
-    // [main] {f} [g,h]
+    // [main] {f} [g,h] (4 times)
     __goblint_check(f(4) == 3); // UNKNOWN
 }

tests/regression/81-loopfree_callstring/11-value_update_sens.c

@@ -0,0 +1,23 @@
+// PARAM: --set "ana.activated[+]" loopfree_callstring --enable ana.int.interval_set
+// Basic example
+#include <stdio.h>
+
+int a = 20;
+
+int f(int i)
+{
+    if (i > 0)
+    {
+        a = --i;
+        f(i);
+    }
+    return 0;
+}
+
+int main(void)
+{
+    // main -> f(10) -> f(9) -> ... f(0)
+    // [main, f] and [main] {f}
+    f(1);
+    __goblint_check(a == 0);
+}

tests/regression/81-loopfree_callstring/12-value_update_ins.c

@@ -0,0 +1,23 @@
+// PARAM: --set "ana.activated[+]" loopfree_callstring  --enable ana.int.interval_set
+// Basic example
+#include <stdio.h>
+
+int a = 20;
+
+int f(int i)
+{
+    if (i > 0)
+    {
+        a = --i;
+        f(i);
+    }
+    return 0;
+}
+
+int main(void)
+{
+    // main -> f(10) -> f(9) -> ... f(0)
+    // [main, f] and [main] {f} (2 times)
+    f(2);
+    __goblint_check(a == 0); // UNKNOWN
+}

tests/regression/81-loopfree_callstring/13-circle_call_and_big_loop.c

@@ -0,0 +1,42 @@
+// PARAM: --set "ana.activated[+]" loopfree_callstring --enable ana.int.interval_set
+// Checks proper handling of recursions in loops + shows that not all 200 iterations are analyzed
+#include <stdio.h>
+
+int f(int i);
+
+int g(int i)
+{
+    if (i == 0)
+    {
+        return 1;
+    }
+    if (i > 0)
+    {
+        return f(i - 1);
+    }
+    return 11;
+}
+
+int f(int i)
+{
+    if (i == 0)
+    {
+        return 2;
+    }
+    if (i > 0)
+    {
+        return g(i - 1);
+    }
+    return 12;
+}
+
+int main(void)
+{
+    for (int i = 200; i > 0; i--)
+    {
+        int res1 = f(2);
+        int res2 = g(2);
+        __goblint_check(res1 == 2);
+        __goblint_check(res2 == 1);
+    }
+}

tests/regression/81-loopfree_callstring/14-loop_unrolling.c

@@ -0,0 +1,26 @@
+// PARAM: --set "ana.activated[+]" loopfree_callstring --enable ana.int.interval_set --set exp.unrolling-factor 3
+
+#include <stdio.h>
+
+int f(int i)
+{
+    if (i == 0)
+    {
+        return 1;
+    }
+    if (i > 0)
+    {
+        return f(i - 1);
+    }
+    return 11;
+}
+
+int main(void)
+{
+    for (int i = 5; i > 0; i--)
+    {
+        // main -> f(3) -> ... -> f(0) -> return 1
+        // [main, f] and {f} (3 times)
+        __goblint_check(f(3) == 1);
+    }
+}

tests/regression/81-loopfree_callstring/15-threads_sens.c

@@ -0,0 +1,84 @@
+// PARAM: --set "ana.activated[+]" loopfree_callstring --enable ana.int.interval_set
+#include <pthread.h>
+#include <stdio.h>
+#include <goblint.h>
+
+int f(int i)
+{
+  if (i == 0)
+  {
+    return 1;
+  }
+  if (i > 0)
+  {
+    return f(i - 1);
+  }
+  return 11;
+}
+
+int g(int i)
+{
+  if (i == 0)
+  {
+    return 3;
+  }
+  if (i > 0)
+  {
+    return g(i - 1);
+  }
+  return 13;
+}
+
+int h(int i)
+{
+  if (i == 0)
+  {
+    return 2;
+  }
+  if (i > 0)
+  {
+    return g(i - 1);
+  }
+  return 12;
+}
+
+int procedure(int num_iterat)
+{
+  int res1 = f(num_iterat);
+  int res2 = g(num_iterat);
+  int res3 = h(num_iterat);
+  int res4 = h(num_iterat);
+  return res1 + res2 + res3 + res4;
+}
+
+void *t_sens(void *arg)
+{
+  // main -> t_sens -> procedure -> f(0)
+  // main -> t_sens -> procedure -> g(0)
+  // main -> t_sens -> procedure -> h(0)
+  __goblint_check(procedure(0) == 8);
+  return NULL;
+}
+
+void *t_sens2(void *arg)
+{
+  // main -> t_sens2 -> procedure -> f(3) -> ... -> f(0)
+  // [main, t_sens2, procedure, f] and [main, t_sens2, procedure] {f} (3 times)
+  // main -> t_sens2 -> procedure -> g(3) -> ... -> g(0)
+  // [main, t_sens2, procedure, g] and [main, t_sens2, procedure] {g} (3 times)
+  // main -> t_sens2 -> procedure -> h(3) -> g(2) -> ... -> g(0)
+  // [main, t_sens2, procedure, h, g] and [main, t_sens2, procedure, h] {g} (2 times)
+  __goblint_check(procedure(3) == 10);
+  return NULL;
+}
+
+int main()
+{
+  pthread_t id;
+  pthread_t id2;
+
+  // Create the thread
+  pthread_create(&id, NULL, t_sens, NULL);
+  pthread_create(&id2, NULL, t_sens2, NULL);
+  return 0;
+}

tests/regression/81-loopfree_callstring/16-threads_ins.c

@@ -0,0 +1,71 @@
+// PARAM: --set "ana.activated[+]" loopfree_callstring  --enable ana.int.interval_set
+#include <pthread.h>
+#include <stdio.h>
+#include <goblint.h>
+
+int f(int i)
+{
+  if (i == 0)
+  {
+    return 1;
+  }
+  if (i > 0)
+  {
+    return f(i - 1);
+  }
+  return 11;
+}
+
+int g(int i)
+{
+  if (i == 0)
+  {
+    return 3;
+  }
+  if (i > 0)
+  {
+    return g(i - 1);
+  }
+  return 13;
+}
+
+int h(int i)
+{
+  if (i == 0)
+  {
+    return 2;
+  }
+  if (i > 0)
+  {
+    return g(i - 1);
+  }
+  return 12;
+}
+
+int procedure(int num_iterat)
+{
+  int res1 = f(num_iterat);
+  int res2 = g(num_iterat);
+  int res3 = h(num_iterat);
+  int res4 = h(num_iterat);
+  return res1 + res2 + res3 + res4;
+}
+
+void *t_ins(void *arg)
+{
+  // main -> t_ins -> procedure -> f(12) -> ... -> f(0)
+  // [main, t_ins, procedure, f] and [main, t_ins, procedure] {f} (12 times)
+  // main -> t_ins -> procedure -> g(12) -> g(11) -> ... -> g(0)
+  // main -> t_ins -> procedure -> h(12) -> g(11) -> ... -> g(0)
+  __goblint_check(procedure(12) == 10); // UNKNOWN
+  return NULL;
+}
+
+int main()
+{
+  pthread_t id;
+
+  // Create the thread
+  pthread_create(&id, NULL, t_ins, NULL);
+  return 0;
+}