From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 3987 invoked by alias); 16 Oct 2006 18:22:24 -0000 Received: (qmail 3976 invoked by uid 22791); 16 Oct 2006 18:22:23 -0000 X-Spam-Check-By: sourceware.org Received: from mx2.palmsource.com (HELO mx2.palmsource.com) (12.7.175.14) by sourceware.org (qpsmtpd/0.31) with ESMTP; Mon, 16 Oct 2006 18:22:18 +0000 Received: from localhost (localhost [127.0.0.1]) by localhost.domain.tld (Postfix) with ESMTP id BB38527AC3; Mon, 16 Oct 2006 11:22:17 -0700 (PDT) Received: from mx2.palmsource.com ([127.0.0.1]) by localhost (mx2.palmsource.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 14778-11-57; Mon, 16 Oct 2006 11:22:16 -0700 (PDT) Received: from ussunex01.palmsource.com (unknown [192.168.101.9]) by mx2.palmsource.com (Postfix) with ESMTP id 9628127A3B; Mon, 16 Oct 2006 11:22:16 -0700 (PDT) Received: from 192.168.92.75 ([192.168.92.75]) by ussunex01.palmsource.com ([192.168.101.9]) via Exchange Front-End Server owa.palmsource.com ([10.0.20.17]) with Microsoft Exchange Server HTTP-DAV ; Mon, 16 Oct 2006 18:22:16 +0000 Received: from svmsnyderlnx by owa.palmsource.com; 16 Oct 2006 11:22:14 -0700 Subject: Re: Light Formal Methods in GDB From: Michael Snyder To: Rob Quill Cc: gdb@sourceware.org In-Reply-To: References: <1160682474.14535.188.camel@localhost.localdomain> <1160765208.14535.251.camel@localhost.localdomain> Content-Type: text/plain Content-Transfer-Encoding: 7bit Date: Mon, 16 Oct 2006 18:22:00 -0000 Message-Id: <1161022934.14535.333.camel@localhost.localdomain> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 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/msg00117.txt.bz2 On Mon, 2006-10-16 at 11:18 +0100, Rob Quill wrote: > On 13/10/06, Michael Snyder wrote: > > > > OK. Well, once you have your list of nodes and properties (values), > > maybe you could have your software emit a set of breakpoint definitions > > for gdb, with appropriate rules for evaluating sets of values at each > > breakpoint. Gdb already has a scripting language that includes "if" > > and "while", and you can define debugger-local variables to define > > your finite automaton and control its state. Then, depending on those > > state variables, gdb can stop the program or let it continue. You > > can also include "print" statements to log your state. > > > > This sounds like an interesting project, and I don't think > > it should require any modifications to gdb (or at least, any > > major ones). You would generate a script for gdb to set up > > the breakpoints and states, then run gdb in batch mode with > > the output piped into a file. You would then post-process > > that file for your results. > > 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. Sure. First compose all the rules for your automaton. Then you can compose a gdb script file that might look, in part, something like this: # Create automaton using GDB user-defined variables set $automaton_state = 0 set $automaton_value1 = 17 set $automaton_value2 = 44 # etc. # Set up breakpoints to manage state transitions break foo commands silent if (program_var1 > program_var2) && (program_var3 == 0) set $automaton_state = 22 end end Consult the gdb docs and runtime help to learn about the macro command language. > 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. Yep!