[bitc-dev] Relevant information

[Sandro Magi]

Jonathan S. Shapiro wrote:

>The basis of their work is automated region inference. Region inference
>isn't going to work for the applications we are really concerned about,
>because the inference engine will conclude (correctly) that the region
>remains live nearly everywhere that we might call free().
>
>So: this is definitely a useful auxiliary technique for BitC, but it
>doesn't address the core issues of memory (de)allocation that we need to
>solve.
>

I see. I wonder, is it possible to have 'compilation
profiles/environments' such that you can restrict compilation strategy
to a definable set of techniques? For instance, let's suppose I wanted a
program to be statically verifiable under the above region inference
technique, could I specify this somehow? I imagine this sort of facility
might be useful. I hope I'm being clear; I'm struggling a little for the
words to express precisely what I mean.

Also, have you looked at LLVM as a foundation for bitc, or do you have a
some other foundation you're using? I'm curious what others think of it.

Sandro