From owner-cvs-src@FreeBSD.ORG Mon Jul 28 13:49:52 2003 Return-Path: Delivered-To: cvs-src@freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id 20E2337B401; Mon, 28 Jul 2003 13:49:52 -0700 (PDT) Received: from mail.tcoip.com.br (erato.tco.net.br [200.220.254.10]) by mx1.FreeBSD.org (Postfix) with ESMTP id 18AE843FA3; Mon, 28 Jul 2003 13:49:49 -0700 (PDT) (envelope-from dcs@tcoip.com.br) Received: from tcoip.com.br ([10.0.2.6]) by mail.tcoip.com.br (8.11.6/8.11.6) with ESMTP id h6SKnQj23353; Mon, 28 Jul 2003 17:49:26 -0300 Message-ID: <3F258C55.6090706@tcoip.com.br> Date: Mon, 28 Jul 2003 17:49:25 -0300 From: "Daniel C. Sobral" User-Agent: Mozilla/5.0 (X11; U; FreeBSD i386; en-US; rv:1.4) Gecko/20030702 X-Accept-Language: en-us, en, pt-br, ja MIME-Version: 1.0 To: Poul-Henning Kamp References: <62633.1059304135@critter.freebsd.dk> In-Reply-To: <62633.1059304135@critter.freebsd.dk> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit cc: Alexander Leidinger cc: src-committers@FreeBSD.org cc: dds@FreeBSD.org cc: cvs-all@FreeBSD.org 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 X-BeenThere: cvs-src@freebsd.org X-Mailman-Version: 2.1.1 Precedence: list List-Id: CVS commit messages for the src tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 28 Jul 2003 20:49:52 -0000 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."