From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <yoriyuki.y@gmail.com>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.9 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE,
	SPF_NEUTRAL autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id A392EBC68
	for <caml-list@yquem.inria.fr>; Sat, 23 Sep 2006 20:05:45 +0200 (CEST)
Received: from py-out-1112.google.com (py-out-1112.google.com [64.233.166.176])
	by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k8NI5ipe028194
	for <caml-list@inria.fr>; Sat, 23 Sep 2006 20:05:45 +0200
Received: by py-out-1112.google.com with SMTP id f25so1680346pyf
        for <caml-list@inria.fr>; Sat, 23 Sep 2006 11:05:44 -0700 (PDT)
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws;
        s=beta; d=gmail.com;
        h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition;
        b=qbDATNEHhHXI96mwUBsvdml3El3o/Wo2uon97+6sV8bbABPjCQPdgYMQg9rLUNs4GnWtTfGABA5NTPaNdM8S3/3HFhUkLJsChhSMyZ13ySl9l1imTKyD0H5Bg8SUoeURVMiojyI0yZWmb1GCmLqEV6cyPj+Fox9lGIRbULiyAwE=
Received: by 10.35.8.13 with SMTP id l13mr3621920pyi;
        Sat, 23 Sep 2006 11:05:43 -0700 (PDT)
Received: by 10.35.71.15 with HTTP; Sat, 23 Sep 2006 11:05:42 -0700 (PDT)
Message-ID: <ace6b6830609231105s13e852ddvf86a777f4f2bc3ce@mail.gmail.com>
Date: Sun, 24 Sep 2006 03:05:43 +0900
From: "Yoriyuki Yamagata" <yoriyuki.y@gmail.com>
To: "Caml List" <caml-list@inria.fr>
Subject: [ANN]BrainScan - A source-code model checker for BrainF*ck
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
X-j-chkmail-Score: MSGID : 45157778.000 on concorde : j-chkmail score : X : 0/20 1
X-Miltered: at concorde with ID 45157778.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; yoriyuki:01 yamagata:01 yoriyuki:01 source-code:01 model:01 checker:01 source-code:01 model:01 checker:01 depth-first:01 buffer:01 ocaml:01 findlib:01 binary:01 underflow:01 

BrainScan is a simple source-code model checker for BrainF*ck.  It
uses depth-first search with states in the buffer cells represented as
sets of integer intervals.

To compile, you need OCaml, findlib, and extlib.
$ make
This create a binary called brainscan.  Then you can give BrainF*ck
program as the argument.

$ ./brainscan '+[]!'
$

BrainScan checks the following condition and prints the command trace
if such conditions could arise.

1. Underflow of the pointer
2. Overflow (> 255) and Underflow (<0) of a buffer-cell value.  (Only
with -R or --range option.)
3. Reach the positions marked by !

In the case above, the program infinitely loops between [ and ].
Hence it never reaches !.  BrainScan understands this, and terminates
without error messages.  On the other hand,

$ ./brainscan ',[]!'
! reached.
        0: ,
        1: [
        3: !

this program may reach ! depending on the input at the ",".

Enjoy!
-- 
Yamagata Yoriyuki