This is the mail archive of the
gcc@gcc.gnu.org
mailing list for the GCC project.
Re: Control Flow Graphs
Thanks very much. I am planning to use this output to help me add some
debugging features to GDB, involving temporal logic, but the
optimizations involve using a CFG. The dream for my project would be
to add an option to GC to print the CFG data to a file, and then parse
it and do some analysis on it, and pass it on do GDB to go some light
formal methods.
I attach below my email to the GDB mailinglist about the aims of the
project, for those who are interseted and have not seen it already.
Any feedback you have is much appreciated.
-------------------------
Hi,
The principle works as follows:
It it possible to create an automaton from an LTL formula, with
expressions for values of variables as the transitions from one state
to the next.
Then the tricky part is building an automaton which represents the
program. But once you have these it is possible to see if the
automaton 'match' and if they do then the property holds.
With regards to building the system automaton, at the very simplest
you could single step the code, get values of variables at each step
and make an appropriate transition on the automaton. However, this is
obviously very inefficient, and improvements would most likely be made
by building a control flow graph of the program (in some way) and use
the nodes of that graph as the points get get values, or something
like that.
The advantage of including something like this in GDB is that once the
property that the programmer expected to hold becomes false, program
execution can stop and he programmer can use the standard GDB tools.
Well, that'd be the idea anyway.
The original idea was to do the same thing but for concurrent programs
because there is research which says that using LTL formulas and the
automaton technique, you can say whether properties of concurrent
programs hold for all the possible interleavings. However, it was
decided that that was too complicated, so it was narrowed to
non-concurrent programs.
-----------
Thanks again.
Rob
On 16/10/06, Paul Yuan <yingbo.com@gmail.com> wrote:
Call dump_flow_info() defined in cfg.c to output the pred and succ of
each block. You can use this output to construct the CFG.
Maybe the software graphviz can help you to visualize the CFG.
On 10/16/06, Rob Quill <rob.quill@gmail.com> wrote:
> Hi,
>
> Does anyone know if it is possible to view/access/print out the
> control flow graphs produced by GCC, either at compilation time, or
> after compilation has taken place?
>
> Thanks for your time.
>
> Rob
>
--
Paul Yuan
www.yingbo.com