Date: Mon, 28 Jul 2003 17:49:25 -0300 From: "Daniel C. Sobral" <dcs@tcoip.com.br> To: Poul-Henning Kamp <phk@phk.freebsd.dk> Cc: cvs-src@FreeBSD.org Subject: Re: 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 Message-ID: <3F258C55.6090706@tcoip.com.br> In-Reply-To: <62633.1059304135@critter.freebsd.dk> References: <62633.1059304135@critter.freebsd.dk>
next in thread | previous in thread | raw e-mail | index | archive | help
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@tco.net.br
Daniel.Sobral@tcoip.com.br
dcs@tcoip.com.br
Outros:
dcs@newsguy.com
dcs@freebsd.org
capo@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."
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?3F258C55.6090706>