Option --replace-calls to replace function calls with calls to other given functions

Author: danpoe

regression/cbmc/replace-calls-01/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int f(int a)
+{
+  return a;
+}
+
+int g(int b)
+{
+  return b + 1;
+}
+
+int main()
+{
+  int r;
+
+  r = f(0);
+  assert(r == 1);
+}

regression/cbmc/replace-calls-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-calls f:g
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/replace-calls-01/main.c

@@ -0,0 +1,18 @@
+
+int f(int a)
+{
+  return a;
+}
+
+int g(int b)
+{
+  return b + 1;
+}
+
+int main()
+{
+  int r;
+
+  r = f(0);
+  assert(r == 1);
+}

regression/goto-instrument/replace-calls-01/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-calls f:g
+g\(0\);
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+f\(0\);
+^warning: ignoring

regression/goto-instrument/replace-calls-02/main.c

@@ -0,0 +1,31 @@
+
+int f()
+{
+  return 0;
+}
+
+int g()
+{
+  return 1;
+}
+
+int h()
+{
+  return 2;
+}
+
+int i()
+{
+  return 3;
+}
+
+int main()
+{
+  int r;
+
+  r = f();
+  assert(r == 1);
+
+  r = h();
+  assert(r == 3);
+}

regression/goto-instrument/replace-calls-02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-calls f:g --replace-calls h:i
+g\(\);
+i\(\);
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+f\(\);
+h\(\);
+^warning: ignoring

regression/goto-instrument/replace-calls-03/main.c

@@ -0,0 +1,15 @@
+
+int f()
+{
+  return 0;
+}
+
+char g()
+{
+  return 1;
+}
+
+int main()
+{
+  f();
+}

regression/goto-instrument/replace-calls-03/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-calls f:g
+Functions f and g are not type-compatible
+^EXIT=11$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/replace-calls-04/main.c

@@ -0,0 +1,15 @@
+
+void f(int a)
+{
+  return 0;
+}
+
+void g(unsigned a)
+{
+  return 1;
+}
+
+int main()
+{
+  f(0);
+}

regression/goto-instrument/replace-calls-04/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-calls f:g
+Functions f and g are not type-compatible
+^EXIT=11$
+^SIGNAL=0$
+--
+^warning: ignoring