source: etc/campbell/dev-notes/2012-02-06-RTLabs-as-after-return.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 631 bytes
Line 
1I still need to prove the as_after_return property for RTLabs, namely that the
2label of the next instruction to execute after a return is the successor of the
3corresponding call.  The only link between the new state and the original is
4the result from the recursive call to build the subtrace for the call.  Thus
5this must somehow show that the frame stack is preserved.  Note that the end
6of this trace will involve dropping the newly created frame.
7
8So, modify the result record type to take the start state as a parameter, and
9require the end state to have the same frame stack, up to dropping the current
10frame if we returned.
Note: See TracBrowser for help on using the repository browser.