Add regression tests for SM typecheck.

Author: NlightNFotis

regression/cbmc-shadow-memory/intrinsics_warnings1/intrinsics_warn.c

@@ -0,0 +1,32 @@
+//
+// Created by Fotis Koutoulakis on 19/09/2023.
+//
+#include <assert.h>
+#include <stdio.h>
+
+struct S
+{
+  int i;
+  int j;
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized", (char)0);
+  __CPROVER_field_decl_global("uninitialized-global", (char)0);
+
+  struct S s;
+  char a;
+
+  __CPROVER_set_field(&a, "uninitialized", 1);
+
+  assert(__CPROVER_get_field(&a, "uninitialized") == 1);
+
+  __CPROVER_set_field(&s, "uninitialized", 1);
+
+  assert(__CPROVER_get_field(&s, "uninitialized") == 1);
+  assert(__CPROVER_get_field(&s.i, "uninitialized") == 1);
+  assert(__CPROVER_get_field(&s.j, "uninitialized") == 1);
+
+  return 0;
+}

regression/cbmc-shadow-memory/intrinsics_warnings1/test.desc

@@ -0,0 +1,16 @@
+CORE
+intrinsics_warn.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+WARNING: no body for function
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_global' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_local' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_set_field' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_get_field' is not declared
+--
+This test is making sure that we don't get any of the log messages warning
+for the shadow memory intrinsics being undefined after the type check phase.

regression/cbmc-shadow-memory/intrinsics_warnings2/test.desc

@@ -0,0 +1,18 @@
+CORE
+typechecking_warning.c
+
+^EXIT=6$
+^SIGNAL=0$
+^CONVERSION ERROR$
+file typechecking_warning\.c line \d function main: __CPROVER_field_decl_local argument 2 must be a byte-sized integer, but \(10ul\) has type `unsigned long int`
+--
+^warning: ignoring
+WARNING: no body for function
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_global' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_local' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_set_field' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_get_field' is not declared
+--
+This test is part of a suite of tests we have for ensuring that the typechecker
+comes up with proper error messages in the case of shadow memory intrinsics
+failing the typechecking phase.

regression/cbmc-shadow-memory/intrinsics_warnings2/typechecking_warning.c

@@ -0,0 +1,9 @@
+//
+// Created by Fotis Koutoulakis on 19/09/2023.
+//
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized", 10ul);
+
+  return 0;
+}

regression/cbmc-shadow-memory/intrinsics_warnings3/test.desc

@@ -0,0 +1,18 @@
+CORE
+typechecking_warning.c
+
+^EXIT=6$
+^SIGNAL=0$
+^CONVERSION ERROR$
+file typechecking_warning\.c line \d function main: __CPROVER_field_decl_local takes exactly 2 arguments, but 1 were provided
+--
+^warning: ignoring
+WARNING: no body for function
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_global' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_local' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_set_field' is not declared
+file intrinsics_warn.c line \d+ function main: function '__CPROVER_get_field' is not declared
+--
+This test is part of a suite of tests we have for ensuring that the typechecker
+comes up with proper error messages in the case of shadow memory intrinsics
+failing the typechecking phase.

regression/cbmc-shadow-memory/intrinsics_warnings3/typechecking_warning.c

@@ -0,0 +1,9 @@
+//
+// Created by Fotis Koutoulakis on 19/09/2023.
+//
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized");
+
+  return 0;
+}