KNOWNBUG test for goto-symex' auto-objects feature

This code partly works, though perhaps not quite as intended. The test
may serve as basis of discussion for how it actually should work.

Author: tautschnig

regression/cbmc/auto_objects1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  int x;
+  int **auto_object_source1;
+  if(*auto_object_source1) // triggers creating an auto object
+  {
+    *auto_object_source1 = &x; // should use the auto object
+    **auto_object_source1 = 42;
+    __CPROVER_assert(x == 42, "42");
+  }
+}

regression/cbmc/auto_objects1/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+--program-only
+auto_object1#\d+ == &x!0@1
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+auto_object_source1\$object#\d+ == &x!0@1
+--
+Dereferencing should eventually use the generated auto-object instead of the
+dereferencing-generated $object.

regression/validate-trace-xml-schema/check.py

@@ -37,6 +37,7 @@
     ['Pointer_Arithmetic19', 'test.desc'],
     ['Quantifiers-simplify', 'simplify_not_forall.desc'],
     ['array-cell-sensitivity15', 'test.desc'],
+    ['auto_objects1', 'test.desc'],
     ['saturating_arithmetric', 'output-formula.desc'],
     # these test for invalid command line handling
     ['bad_option', 'test_multiple.desc'],