Re: Super Lint (was: Unexecutable Stack / Buffer Overflow

Brandon S. Allbery KF8NH (allbery@kf8nh.apk.net)
Mon, 3 Jan 2000 04:34:06 +0200

In message <386ffbb9.26318170@mail.mbay.net>, John Alvord writes:
+-----
| The real challenge extends beyond proving C programs correct. Linux
| has many environments which have implicit preconditions. Cases where
| the code should never go into a wait. What with the preprocessor,
| interrupts,locking, inline functions, and a() calling b() calling c()
| calling d(), verifying the implicit preconditions is tough. That is
| what a Linux-lint should be targetted at, IMHO.
+--->8

I remain somewhat surprised that nobody has added __attribute__ clauses to
gcc to implement programming-by-contract (precondition, postcondition, and
invariant clauses). This would have the advantage that test kernels could
be built with the clauses enabled (potential speed hit) and release kernels
could have them disabled by default, as well as documenting the requirements
of a function.

-- 
brandon s. allbery	   os/2,linux,solaris,perl	allbery@kf8nh.apk.net
system administrator	   kthkrb,heimdal,gnome,rt	  allbery@ece.cmu.edu
carnegie mellon / electrical and computer engineering			kf8nh
    We are Linux. Resistance is an indication that you missed the point.






-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/