added test for values in traces

Author: kroening

regression/cbmc/trace-values/trace-values.c

@@ -0,0 +1,38 @@
+int global_var;
+
+struct S
+{
+  int f;
+  int array[3];
+} my_nested[2];
+
+int main()
+{
+  static int static_var;
+  int local_var;
+  int *p=&my_nested[0].array[1];
+  int *q=&my_nested[1].f;
+  int *null=0;
+  int *junk;
+
+  global_var=1;
+  static_var=2;
+  local_var=3;
+  *p=4;
+  *q=5;
+  *null=6;
+  *junk=7;
+
+  // dynamic
+  p=malloc(sizeof(int)*2);
+  p[1]=8;
+  
+  // not even a pointer variable
+  *(int *)0=9;
+
+  // assign entire struct
+  my_nested[1]=my_nested[0];
+
+  // get a trace
+  __CPROVER_assert(0, "");
+}

regression/cbmc/trace-values/trace-values.desc

@@ -0,0 +1,18 @@
+CORE
+trace-values.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^  local_var=0 .*$
+^  global_var=1 .*$
+^  static_var=2 .*$
+^  local_var=3 .*$
+^  my_nested\[0.*\].array\[1.*\]=4 .*$
+^  my_nested\[1.*\].f=5 .*$
+^  null\$object=6 .*$
+^  junk\$object=7 .*$
+^  dynamic_object1\[1.*\]=8 .*$
+^  my_nested\[1.*\]={ .f=0, .array={ 0, 4, 0 } } .*$
+^VERIFICATION FAILED$
+--
+^warning: ignoring