The SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported:

https://blog.adacore.com/pointer-based-data-structures-in-sp...

Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)