Messages in this thread | | | Date | Fri, 30 May 2003 11:30:09 -0300 | From | Werner Almesberger <> | Subject | Re: inventing the wheel? |
| |
Carl-Daniel Hailfinger wrote: > Now we only need one additional tool to *prove* correctness of the > kernel ;-)
Perhaps another interesting approach for such source code analyzers would be to take a top-down view, i.e. assume a certain functional structure, and check that all the elements are there and in the right order.
This should be feasible for code that basically follows a certain template, e.g. network card drivers.
This would also help with the update problem of "fill in the blanks" type of templates, i.e. if the template changes or is augmented, some drivers using it may no longer conform to it.
Such a top-down view could be layered on top of a bottom-up analyzer, e.g. by - manually or automatically - translating some "skeleton" into a set of rules of the type "if you've called X, you must later call Y", etc.
- Werner
-- _________________________________________________________________________ / Werner Almesberger, Buenos Aires, Argentina wa@almesberger.net / /_http://www.almesberger.net/____________________________________________/ - To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
| |