-
Notifications
You must be signed in to change notification settings - Fork 7
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Issues in 4.0 port via the ilist iterators #2
Comments
Dsa-seahorn is a fork of the original DSA analysis that was part of the pollalloc project. We have recently implemented an improved version of DSA which is part of seahorn. We plan to get rid of dsa-seahorn soon so I wouldn't spent time porting it. We also plan to replace dsa-seahorn in crab-llvm. You can compile both seahorn and crab-llvm without dsa-seahorn. The only limitation is that you won't be able to reason about memory. I strongly recommend to skip dsa-seahorn. |
Hey @jcarlson23, we much appreciate your help with porting the code to LLVM 4.0. This is a non-trivial task :) If the notion of GraphTrait has changed in LLVM, then LLVM mainline had to update their code appropriately. You can probably find the right solution by looking at the diff between LLVM 3.6 and LLVM 4.0 for other implementations of GraphTrait in LLVM mainline. A good example would be GraphTraits for Control Flow Graph. In LLVM 3.6, it is located in |
Thanks guys! @caballa I'm going to take your suggestion (that speeds things up quite nicely anyway) so that works well for me. Thanks again! |
Hello, I'm trying to port this to 4.0 (as part of a Crab port) and I'm having issues in that the 4.0 GraphTraits requires
NodeRef
to be a pointer, and so I gettypedef DSNode* NodeRef
. For example in dsa-seahorn/include/dsa/GraphTraits.h I changed NodeType referring to a DSNode instead to point to a DSNode:This seems to fix a number of issues for the node itself but when I go into DSGraph then I need iterators that can be dereferenced as NodeRef's...
I reached out to the mailing list and got the following:
So I'm trying to reimplement using the following type of fix (in DSGraph.h):
This is failing mostly in the instantiation of the ilist and I have to confess that I don't quite understand the
ilist_sentinel_traits<DSNode>
that was there (this was deprecated now so I changed that tosimple_ilist<DSNode>
, thensimple_ilist<DSNode*>
as I've understand the code a bit better and GraphTraits...So, am I correct that given NodeRef being required to be a pointer the ilist_traits need to be implemented? Was that
list_sentinel_traits<DSNode>
giving you the quick sentinel and head creation needed for iteration? I've got a fork you can look at directly if you'd like but, it just feels like a lot of behind the scenes code gets pulled in and while I'm relatively confident that the NodeRef issues are moving along that's bumping into other problems.... Any help would be appreciated.The text was updated successfully, but these errors were encountered: