On Wed, 2008-10-08 at 10:02 +0200, Lorens Kockum wrote: > 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.
const has no meaning in BitC. const has no *useful* meaning in C. The problem is that const is not part of type. It is an attribute of a reference. The result is that you can have both const and non-const paths to the same datum, with the result that the compiler cannot really make much use of const. In any case, const is a purely local property, so it isn't really related to this issue. > 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? No. It is intended as a construction aid for deeply embedded systems that must operate without *any* heap, or with a very tightly bounded heap. > 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. This does not scale gracefully to millions of lines of code, even if you have all of the source ready to hand. It also pushes the detection of property failure to post-link phase. I think the real issue here is that the price of avoiding syntactic cruft is to detect the failure later in the compiler cycle. This is actually a very useful thing to realize, and I hadn't seen it before this morning. > 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"... These are much harder properties. "Don't allocate at all" can be tested syntactically. "Don't leave more than X bytes" requires simulating the execution. That is qualitatively harder and in some cases not solvable at all. > I imagine that would be part of the > "push-down model checking framework"? Not likely. Model checking isn't strong enough to analyze this kind of property most of the time. The property you are describing requires full software verification. It cannot be solved in all programs. Even in programs where it *can* be solved, the answer may come out very very conservative. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
