From owner-cvs-src@FreeBSD.ORG Tue Jul 29 02:25:54 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 9414937B401; Tue, 29 Jul 2003 02:25:54 -0700 (PDT) Received: from mailout07.sul.t-online.com (mailout07.sul.t-online.com [194.25.134.83]) by mx1.FreeBSD.org (Postfix) with ESMTP id 5B44E43F93; Tue, 29 Jul 2003 02:25:53 -0700 (PDT) (envelope-from Alexander@Leidinger.net) Received: from fwd10.aul.t-online.de by mailout07.sul.t-online.com with smtp id 19hQju-000200-0M; Tue, 29 Jul 2003 11:25:50 +0200 Received: from Andro-Beta.Leidinger.net (rPTUsgZ-oecdQgAdOdp4eUWksFvyQkWh6F+bo3Jzo-BS2KjO-Q2+4v@[80.131.124.182]) by fmrl10.sul.t-online.com with esmtp id 19hQjj-0RvYy80; Tue, 29 Jul 2003 11:25:39 +0200 Received: from Magelan.Leidinger.net (Magelan [192.168.1.1]) h6T9Pe9P055629; Tue, 29 Jul 2003 11:25:40 +0200 (CEST) (envelope-from Alexander@Leidinger.net) Received: from Magelan.Leidinger.net (netchild@localhost [127.0.0.1]) by Magelan.Leidinger.net (8.12.9/8.12.9) with SMTP id h6T9PnDb001073; Tue, 29 Jul 2003 11:25:49 +0200 (CEST) (envelope-from Alexander@Leidinger.net) Date: Tue, 29 Jul 2003 11:25:49 +0200 From: Alexander Leidinger To: Poul-Henning Kamp Message-Id: <20030729112549.4bf47e95.Alexander@Leidinger.net> In-Reply-To: <3F258C55.6090706@tcoip.com.br> References: <62633.1059304135@critter.freebsd.dk> <3F258C55.6090706@tcoip.com.br> X-Mailer: Sylpheed version 0.9.3claws (GTK+ 1.2.10; i386-portbld-freebsd5.1) Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Seen: false X-ID: rPTUsgZ-oecdQgAdOdp4eUWksFvyQkWh6F+bo3Jzo-BS2KjO-Q2+4v@t-dialin.net cc: cvs-src@FreeBSD.org cc: src-committers@FreeBSD.org cc: dds@FreeBSD.org cc: cvs-all@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: Tue, 29 Jul 2003 09:25:55 -0000 On Mon, 28 Jul 2003 17:49:25 -0300 "Daniel C. Sobral" wrote: > 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. :-) BTW. it's the second model checker I want to add a port for, I just hadn't the URL at hand at the time I mentioned uppaal. See http://spinroot.com/spin/whatispin.html for more. Bye, Alexander. -- Press every key to continue. http://www.Leidinger.net Alexander @ Leidinger.net GPG fingerprint = C518 BC70 E67F 143F BE91 3365 79E2 9C60 B006 3FE7