cvs commit: src/sys/kern init_main.c kern_malloc.c md5c.c subr_autoconf.c subr_mbuf.c subr_prf.c tty_subr.c vfs_cluster.c vfs_subr.c

[Daniel C. Sobral]

Poul-Henning Kamp wrote:
> 
> Yes I think it would, but you would have to find a way to prove to 
> yourself that your model was in fact precise and faithful relative to
> the kernel source.
> 
> I'm still hoping that some day we will have tools which will read
> source code and alert us to things which doesn't make sense or which
> looks dubious.

Well, that's what I like about Spin. A clever use of macros let you 
pre-process your C code to be "Spinnable" with little to no work. :-)

-- 
Daniel C. Sobral                   (8-DCS)
Gerencia de Operacoes
Divisao de Comunicacao de Dados
Coordenacao de Seguranca
VIVO Centro Oeste Norte
Fones: 55-61-313-7654/Cel: 55-61-9618-0904
E-mail: Daniel.Capo at tco.net.br
         Daniel.Sobral at tcoip.com.br
         dcs at tcoip.com.br

Outros:
	dcs at newsguy.com
	dcs at freebsd.org
	capo at notorious.bsdconspiracy.net

Higgeldy Piggeldy,
Hamlet of Elsinore
Ruffled the critics by
Dropping this bomb:
"Phooey on Freud and his
Psychoanalysis,
Oedipus, Shmoedipus,
I just loved Mom."