On Tue, Oct 07, 2008 at 01:43:22PM -0400, Swaroop Sridhar wrote: > It is possible to add a switch to the compiler so that it will not > perform some of the effect checking (ex: alloc/noalloc), or make some > conservative default assumptions for the lack of programmer annotation. > However, code that must work in either mode (ex: libraries) must be > written in a fully annotated form.
Does the C++ concept "const" have a meaning in BitC? The problem seems to be much the same. Looking at the problem from *way* above, I'd just like to make quite sure I understand the use for noalloc. Is it to make sure that calling some code will not create a memory leak? A kind of confinement at the function level (like const...)? It's not just to avoid memory consumption, since an infinite recursive will consume all the memory you like without any dynamic allocation, right? As I see it, either you have source or you don't. If you have the source, you could place a constraint once, when you need it, and ask the compiler to check all the called code. If you don't have the source, but compiled code that you trust, then you should have the constraint reflected somewhere in the description, much like const is integrated in the type system. In any case I'd have expected to find "don't allocate any memory at all" as a special case of a list containing "don't leave more than X bytes allocated after function exit", "do not use more than X bytes of memory", "do not make any library calls that could change system state", "do not change the memory pointed to by any pointers I might have passed to you", "return in less than x time". Basically, sandbox the function. Of course most of these are much harder to analyze at compile-time than "don't call the memory allocation function", but at the same time they're the ones I would want when calling code I hadn't analyzed myself in detail. I imagine that would be part of the "push-down model checking framework"? -- Lorens _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
