Merge pull request #3058 from hannes-steffenhagen-diffblue/regression-builtin_function_frontend_checks

Some extra tests for do_function_call_symbol

Author: tautschnig

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
+--