Jonathan S. Shapiro wrote: > The BitC compiler currently supports a --noalloc flag, which raises an > error if the unit of compilation being compiled performs allocation. > > This is a useful check, but it can be done in a static analyzer. On the > other hand, it can also be handled with a form of effect typing. > > Question: is non-allocation sufficiently important enough that it should > be part of the in-language type system, or is the use-case for it rare > enough that we should handle it in a static checker?
I can see the usefulness of having it in the language, since it allows code producers and consumers to state and verify invariants in a more fine-grained manner than is possible via an external tool. Then again, this allocate yes/no invariant is pretty coarse-grained, so that will limit its usefulness. > As background to this question, it occurred to me this morning that > effect analysis can be viewed as a degenerate case of control-flow model > checking, I've always thought of it that way: type systems perform dataflow analysis, effect systems perform control flow analysis. Sandro > and it is already my intention to add a push-down model > checking framework to BitC. Those properties would be checked by the > checker rather than the compiler, but they would be checkable in > whole-program form. > > > shap > > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
