Changeset 1617 for src/RTLabs
- Timestamp:
- Dec 14, 2011, 6:17:50 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1601 r1617 567 567 568 568 (* FIXME: there's trouble at the end of the program because we can't make a step 569 away from the final return. *) 569 away from the final return. 570 571 We need to show that the "next pc" is preserved through a function call. 572 573 Tail-calls are not handled properly (which means that if we try to show the 574 full version with non-termination we'll fail because calls and returns aren't 575 balanced. 576 577 The guardedness check will reject the recursive definition above; need to 578 rearrange things so that this works properly. 579 *)
Note: See TracChangeset
for help on using the changeset viewer.