Changeset 1617


Ignore:
Timestamp:
Dec 14, 2011, 6:17:50 PM (8 years ago)
Author:
campbell
Message:

Note stuff to do on structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1601 r1617  
    567567 
    568568(* 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.