RSSA

[Matthew Fluet]

> > There is also the C-calling convention which requires the caller to pop
> > the c-stack of callee arguments.  Technically, this seems like a CReturn
> > type of operation, but we don't know the number and/or size of the
> > arguments there.  It seems really messy to pass an args list to each
> > CReturn.  It's not a big deal; the pop is trivial (i.e., won't touch
> > any registers besides %esp) and can be done before transfering to the
> > CReturn.
> 
> Fine.  But I don't mind adding it to the CReturn as well.

O.k.  Here's a more serious concern.  Many of the primitives that are
implemented via Ccalls (the impCCall predicate) need to work with the
returned value; e.g., all the intInf operations are implemented as
C-calls, but after returning from C, I need to update the frontier and
extract the real result.  So, I think CReturn needs a Prim.t, so I know
what to do; that gets messy, because it means that the implementation of a
lot of primitives need be split into what to do at the CCall and what to
do at the CReturn.