Re: [fstar-club] kremlin question: define struct

2017-05-05 Thread zhiting zhu via fstar-club
Hi Jonathan, Thanks for the reply. I have filed the bug in the github issues. Best, Zhiting On Fri, May 5, 2017 at 7:47 AM, Jonathan Protzenko wrote: > HI Zhiting, > > > This is a use-case that no one has ever exercised so far, meaning that the > translation is lacking.

Re: [fstar-club] KreMLin question about allocation on the heap

2017-05-05 Thread Jonathan Protzenko via fstar-club
Hi Zhiting, We haven't spent a lot of time and effort modeling heap-based allocation, although I believe there's no theoretical reason why we can't do it. It's just that we've been using stack-based allocation for most of our code, so far... perhaps we could have one of our interns over the