search

seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Print the dot file for a graph #69

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello sea-dsa developers,

I'd like to print the dot file for a graph in an internal pass of SMACK. It seems that the only proper API to do this is createDsaPrinterPass. Using this function requires the pass manager to be available, which I don't know how to get within an LLVM pass. So I was wondering if you could share some pointers about how I should proceed. I think that declaring the pass createDsaPrinterPass returns in a header file should work.

caballa commented 4 years ago

Just need to follow what we do for method viewGraph (https://github.com/seahorn/sea-dsa/blob/master/include/sea_dsa/Graph.hh#L267) Add a new method in class Graph that does exactly the same that viewGraph but without launching the viewer. Note that the actual implementation of viewGraph is actually defined in https://github.com/seahorn/sea-dsa/blob/master/src/DsaPrinter.cc#L750 .

shaobo-he commented 4 years ago

Just need to follow what we do for method viewGraph (https://github.com/seahorn/sea-dsa/blob/master/include/sea_dsa/Graph.hh#L267) Add a new method in class Graph that does exactly the same that viewGraph but without launching the viewer. Note that the actual implementation of viewGraph is actually defined in https://github.com/seahorn/sea-dsa/blob/master/src/DsaPrinter.cc#L750 .

Thank you for your reply. Should I submit a PR for this since it requires modification in the Graph class?

caballa commented 4 years ago

Yes, please.

shaobo-he commented 4 years ago

Closes via 855c78b.