Add test for shadow memory of getenv

We must be able to attach memory to the memory
returned by getenv().

Author: peterschrammel

regression/cbmc-shadow-memory/getenv1/main.c

@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+void main()
+{
+  __CPROVER_field_decl_global("dr_write", (_Bool)0);
+
+  char *env = getenv("PATH");
+  __CPROVER_assume(env != NULL);
+  assert(!__CPROVER_get_field(env, "dr_write"));
+
+  __CPROVER_set_field(env, "dr_write", 1);
+  assert(__CPROVER_get_field(env, "dr_write"));
+}

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

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring