Re: Light Formal Methods in GDB

[Daniel Jacobowitz <drow@false.org>]

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