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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> 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
