From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 20499 invoked by alias); 16 Oct 2006 14:38:10 -0000 Received: (qmail 20490 invoked by uid 22791); 16 Oct 2006 14:38:09 -0000 X-Spam-Check-By: sourceware.org Received: from nevyn.them.org (HELO nevyn.them.org) (66.93.172.17) by sourceware.org (qpsmtpd/0.31.1) with ESMTP; Mon, 16 Oct 2006 14:38:02 +0000 Received: from drow by nevyn.them.org with local (Exim 4.54) id 1GZTbL-0005NP-Cq; Mon, 16 Oct 2006 10:37:59 -0400 Date: Mon, 16 Oct 2006 14:38:00 -0000 From: Daniel Jacobowitz To: Rob Quill Cc: Michael Snyder , gdb@sourceware.org Subject: Re: Light Formal Methods in GDB Message-ID: <20061016143758.GA20426@nevyn.them.org> Mail-Followup-To: Rob Quill , Michael Snyder , gdb@sourceware.org References: <1160682474.14535.188.camel@localhost.localdomain> <1160765208.14535.251.camel@localhost.localdomain> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.13 (2006-08-11) X-IsSubscribed: yes Mailing-List: contact gdb-help@sourceware.org; run by ezmlm Precedence: bulk List-Subscribe: List-Archive: List-Post: List-Help: , Sender: gdb-owner@sourceware.org X-SW-Source: 2006-10/txt/msg00113.txt.bz2 On Mon, Oct 16, 2006 at 11:18:45AM +0100, Rob Quill wrote: > Hi. > > Could you elaborate on this please. I am confused as to how I could > use the GDB scripting language. Can I say things such as "if val = 1" > then do some transition of the automaton and then single step the > program? Or, say that I has somehow already figured out where I wanted > the breakpoints to be I could just set GDB to break there, make > automaton transitions and then keep going. > > Is that what you meant? Because that sounds excellent and a lot > simpler than trying to build it into GDB some how, which was what I > thought I would have to do. I doubt that you could do it directly in GDB's scripting language; although, it might be possible, with use of the "shell" builtin command (to run another program to cause the automaton to transform). However, it sounds to me like what you really want is an external program in control of GDB. The only tricky part would be "handing off" to the user once you've reached a state where the constraints are violated, but I'm sure that you can find a way to do that. The external program can initially drive GDB through the MI interface, then switch interpreters to the CLI for the user. -- Daniel Jacobowitz CodeSourcery