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 summer improve the situation, since it's something that we will want to do in the long run. In the meanwhile, there are functions called `ecreate` (or perhaps it is `rcreate`?) that allocate in an "eternal" region where things are always live. While this region could be conservatively garbage-collected, the current implementation is to just perform malloc without ever freeing the region. Again, this could (should) be improved. I fixed the test cases yesterday so Travis is green again for KreMLin. Thanks, ~ jonathan ________________________________ From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of zhiting zhu via fstar-club <fstar-club@lists.gforge.inria.fr> Sent: Tuesday, May 2, 2017 2:59:51 PM To: fstar-club@lists.gforge.inria.fr Subject: [fstar-club] KreMLin question about allocation on the heap Hi all, I'm new to F* lang and I'm excited to find out that a subset of F* can be translated to C. After looking through the test example, I couldn't find any of them has heap allocation in the translated C code and I couldn't figure out anyway to write in F* which will translate to C with malloc or calloc. Is the feature supported? Is there a simple example I could look at for reference? I also notice that there are test cases failing... Best, Zhiting
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
