Add tests of alloca declaration validation

Author: thomasspriggs

regression/cbmc-library/alloca_declaration/missing_parameters.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stddef.h>
+
+void *alloca();
+
+int main()
+{
+  int n;
+  __CPROVER_assume(5 <= n && n < 10);
+  int *c = alloca();
+  assert(c);
+  return 0;
+}

regression/cbmc-library/alloca_declaration/missing_parameters.desc

@@ -0,0 +1,11 @@
+CORE
+missing_parameters.c
+
+file missing_parameters\.c line 10 function main: 'alloca' function called, but 'alloca' has not been declared with expected single 'size_t' parameter\.
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is a test for C front end to confirm an appropriate error message is
+generated if `alloca` is called when it is declared without parameters.

regression/cbmc-library/alloca_declaration/too_many_parameters.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stddef.h>
+
+void *alloca(size_t a, size_t b);
+
+int main()
+{
+  int n;
+  __CPROVER_assume(5 <= n && n < 10);
+  int *c = alloca(n * sizeof(int), 42);
+  assert(c);
+  return 0;
+}

regression/cbmc-library/alloca_declaration/too_many_parameters.desc

@@ -0,0 +1,11 @@
+CORE
+too_many_parameters.c
+
+file too_many_parameters\.c line 10 function main: 'alloca' function called, but 'alloca' has not been declared with expected single 'size_t' parameter\.
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is a test for C front end to confirm an appropriate error message is
+generated if `alloca` is called when it is declared with too many parameters.

regression/cbmc-library/alloca_declaration/undeclared.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stddef.h>
+
+int main()
+{
+  int n;
+  __CPROVER_assume(5 <= n && n < 10);
+  int *c = alloca(n * sizeof(int));
+  assert(c);
+  return 0;
+}

regression/cbmc-library/alloca_declaration/undeclared.desc

@@ -0,0 +1,11 @@
+CORE
+undeclared.c
+
+file undeclared\.c line 8 function main: 'alloca' function called, but 'alloca' has not been declared with expected 'void \*' return type\.
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is a test for C front end to confirm an appropriate error message is
+generated if `alloca` is called when it is not declared.

regression/cbmc-library/alloca_declaration/valid_declaration.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stddef.h>
+
+void *alloca(size_t alloca_size);
+
+int main()
+{
+  int n;
+  __CPROVER_assume(5 <= n && n < 10);
+  int *c = alloca(n * sizeof(int));
+  assert(c);
+  return 0;
+}

regression/cbmc-library/alloca_declaration/valid_declaration.desc

@@ -0,0 +1,11 @@
+CORE
+valid_declaration.c
+
+^VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is a test for C front end to confirm that if `alloca` is declared as
+expected then no error is generated.

regression/cbmc-library/alloca_declaration/wrong_parameter_type.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stddef.h>
+
+void *alloca(char);
+
+int main()
+{
+  int n;
+  __CPROVER_assume(5 <= n && n < 10);
+  int *c = alloca(n * sizeof(int));
+  assert(c);
+  return 0;
+}

regression/cbmc-library/alloca_declaration/wrong_parameter_type.desc

@@ -0,0 +1,11 @@
+CORE
+wrong_parameter_type.c
+
+file wrong_parameter_type\.c line 10 function main: 'alloca' function called, but 'alloca' has not been declared with expected single 'size_t' parameter\.
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is a test for C front end to confirm an appropriate error message is
+generated if `alloca` is called when it is declared with too many parameters.