Some extra tests for do_function_call_symbol

These tests show that error conditions in builtin_functions.cpp
are reachable with the right input. Going forward we plan to do
some work to improve the frontend to catch errors like these earlier,
for this purpose it should be helpful to have these tests already in
place.

Author: Petr Bauch

regression/cbmc/assert_func_four/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __assert_func();
+
+  return 0;
+}

regression/cbmc/assert_func_four/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have four arguments
+--

regression/cbmc/assert_lhs/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int n;
+  int m = assert(n > 5);
+
+  return 0;
+}

regression/cbmc/assert_lhs/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected not to have LHS
+--

regression/cbmc/assert_one/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int n;
+  int m = assert(n > 5, 5);
+
+  return 0;
+}

regression/cbmc/assert_one/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have one argument
+--

regression/cbmc/assert_rtn_four/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __assert_rtn();
+
+  return 0;
+}

regression/cbmc/assert_rtn_four/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have four arguments
+--

regression/cbmc/builtin_is/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n, m;
+  __builtin_isgreater(n, m);
+  return 0;
+}

regression/cbmc/builtin_is/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have two float/double arguments
+--

regression/cbmc/builtin_va_copy_lvalue/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n;
+  __builtin_va_copy(5, n);
+  return 0;
+}

regression/cbmc/builtin_va_copy_lvalue/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+argument expected to be lvalue
+--

regression/cbmc/builtin_va_copy_two/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  __builtin_va_copy();
+  return 0;
+}

regression/cbmc/builtin_va_copy_two/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+wrong number of function arguments
+--

regression/cbmc/builtin_va_end_lvalue/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  __builtin_va_end(5);
+  return 0;
+}

regression/cbmc/builtin_va_end_lvalue/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+argument expected to be lvalue
+--

regression/cbmc/builtin_va_end_one/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  __builtin_va_end();
+  return 0;
+}

regression/cbmc/builtin_va_end_one/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+wrong number of function arguments
+--

regression/cbmc/builtin_va_start_lvalue/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n;
+  __builtin_va_start(5, n);
+  return 0;
+}

regression/cbmc/builtin_va_start_lvalue/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+argument expected to be lvalue
+--

regression/cbmc/builtin_va_start_two/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n;
+  __builtin_va_start(n, 5, 5);
+  return 0;
+}

regression/cbmc/builtin_va_start_two/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have two arguments
+--

regression/cbmc/cprover_assert_lhs/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  void m = __CPROVER_assert("n>5", "foo");
+
+  return 0;
+}

regression/cbmc/cprover_assert_lhs/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected not to have LHS
+--

regression/cbmc/cprover_assert_two/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __CPROVER_assert();
+
+  return 0;
+}

regression/cbmc/cprover_assert_two/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+wrong number of function arguments
+--

regression/cbmc/cprover_fence_one/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __CPROVER_fence();
+
+  return 0;
+}

regression/cbmc/cprover_fence_one/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+not enough function arguments
+--

regression/cbmc/cprover_havoc_object_lhs/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int n;
+  void m = __CPROVER_havoc_object(n);
+
+  return 0;
+}

regression/cbmc/cprover_havoc_object_lhs/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected not to have LHS
+--

regression/cbmc/cprover_havoc_object_one/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __CPROVER_havoc_object();
+
+  return 0;
+}

regression/cbmc/cprover_havoc_object_one/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+wrong number of function arguments
+--

regression/cbmc/cprover_input_lhs/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int n;
+  void m = __CPROVER_input(n);
+
+  return 0;
+}

regression/cbmc/cprover_input_lhs/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected not to have LHS
+--

regression/cbmc/cprover_output_lhs/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int n;
+  void m = __CPROVER_output(n);
+
+  return 0;
+}

regression/cbmc/cprover_output_lhs/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected not to have LHS
+--

regression/cbmc/function_not_found/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  foo();
+
+  return 0;
+}

regression/cbmc/function_not_found/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected not to have LHS
+--

regression/cbmc/gcc_builtin_va_arg_one/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int n;
+
+  gcc_builtin_va_arg();
+
+  return 0;
+}

regression/cbmc/gcc_builtin_va_arg_one/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have one argument
+--

regression/cbmc/sync_X_and_fetch_pointer/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n, *m;
+  __sync_add_and_fetch(n, m);
+  return 0;
+}

regression/cbmc/sync_X_and_fetch_pointer/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+primitives take pointer as first argument
+CONVERSION ERROR
+--

regression/cbmc/sync_X_and_fetch_two/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int *n;
+  __sync_add_and_fetch(n);
+  return 0;
+}

regression/cbmc/sync_X_and_fetch_two/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have at least two arguments
+--

regression/cbmc/sync_bool_compare_pointer/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n, *m, *o;
+  __sync_bool_compare_and_swap(n, m, o);
+  return 0;
+}

regression/cbmc/sync_bool_compare_pointer/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have pointer argument
+--

regression/cbmc/sync_bool_compare_three/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int *n, *m;
+  __sync_bool_compare_and_swap(n, m);
+  return 0;
+}

regression/cbmc/sync_bool_compare_three/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have at least three arguments
+--

regression/cbmc/sync_fetch_and_X_pointer/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int n, *m;
+  __sync_fetch_and_add(n, m);
+  return 0;
+}

regression/cbmc/sync_fetch_and_X_pointer/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+primitives take pointer as first argument
+CONVERSION ERROR
+--

regression/cbmc/sync_fetch_and_X_two/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int *n;
+  __sync_fetch_and_add(n);
+  return 0;
+}

regression/cbmc/sync_fetch_and_X_two/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+expected to have at least two arguments
+--