|
Last change
on this file was
3672,
checked in by campbell, 3 years ago
|
|
I'd been keeping some notes in the repo; didn't commit these before
|
|
File size:
375 bytes
|
| Line | |
|---|
| 1 | Something that came up while discussing the presentation of the front-end for |
|---|
| 2 | the review meeting: |
|---|
| 3 | |
|---|
| 4 | It would have been nice to show that any non-terminating function execution |
|---|
| 5 | yields an infinite trace of cost labels. However, this needs the soundness of |
|---|
| 6 | the cost labelling, which might be a little awkward because you'd want the |
|---|
| 7 | result at Clight, but it's checked at RTLabs. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
