<trace> is poorly documented

[davidmalcolm]

I meant <trace> to cover a sequence of events, but I see now that it could be thought of as representing a stack trace. I think I want a separate element for the latter, to distinguish them.

Consider, say:

 1 void foo (void)
 2 {
 3  int tmp = 1;
 4  bar (&tmp);
 5  bar (&tmp);
 6 }
 7
 8 void bar (int *ptr)
 9 {
10   baz (1 / *ptr);
11   *ptr--;
12 }

A checker might want to report this sequence of states:

state 1:
  PC=3
  callstack:
     frame 0: foo; tmp = 1;

state 2:
  PC=4
  callstack:
     frame 0: foo; tmp = 1;

state 3:
  PC=10
  callstack:
     frame 1: bar;
     frame 0: foo; tmp = 1; PC=4

state 4:
  PC=11
  callstack:
     frame 1: bar;
     frame 0: foo; tmp = 1; PC=4

state 5:
  PC=11
  callstack:
     frame 1: bar;
     frame 0: foo; tmp = 1; PC=4

state 6:
  PC=5
  callstack:
     frame 0: foo; tmp = 0; PC=5

state 7:
  PC=10
  callstack:
     frame 1: bar;
     frame 0: foo; tmp = 0; PC=5

with a divide-by-zero here on the 2nd call to "bar".

There's a sequence of states, and each state has a stack of frames associated with it. The data model as it stands can't really directly capture this.