+ ---------
+ -- Vet --
+ ---------
+
+ function Vet (Position : Cursor) return Boolean is
+ begin
+ if Position.Node = null then
+ return Position.Container = null;
+ end if;
+
+ if Position.Container = null then
+ return False;
+ end if;
+
+ -- An invariant of a node is that its Previous and Next components can
+ -- be null, or designate a different node. Also, its element access
+ -- value must be non-null. Operation Free sets the node access value
+ -- components of the node to designate the node itself, and the element
+ -- access value to null, before actually deallocating the node, thus
+ -- deliberately violating the node invariant. This gives us a simple way
+ -- to detect a dangling reference to a node.
+
+ if Position.Node.Next = Position.Node then
+ return False;
+ end if;
+
+ if Position.Node.Prev = Position.Node then
+ return False;
+ end if;
+
+ if Position.Node.Element = null then
+ return False;
+ end if;
+
+ -- In practice the tests above will detect most instances of a dangling
+ -- reference. If we get here, it means that the invariants of the
+ -- designated node are satisfied (they at least appear to be satisfied),
+ -- so we perform some more tests, to determine whether invariants of the
+ -- designated list are satisfied too.
+
+ declare
+ L : List renames Position.Container.all;
+
+ begin
+ if L.Length = 0 then
+ return False;
+ end if;
+
+ if L.First = null then
+ return False;
+ end if;
+
+ if L.Last = null then
+ return False;
+ end if;
+
+ if L.First.Prev /= null then
+ return False;
+ end if;
+
+ if L.Last.Next /= null then
+ return False;
+ end if;
+
+ if Position.Node.Prev = null and then Position.Node /= L.First then
+ return False;
+ end if;
+
+ if Position.Node.Next = null and then Position.Node /= L.Last then
+ return False;
+ end if;
+
+ if L.Length = 1 then
+ return L.First = L.Last;
+ end if;
+
+ if L.First = L.Last then
+ return False;
+ end if;
+
+ if L.First.Next = null then
+ return False;
+ end if;
+
+ if L.Last.Prev = null then
+ return False;
+ end if;
+
+ if L.First.Next.Prev /= L.First then
+ return False;
+ end if;
+
+ if L.Last.Prev.Next /= L.Last then
+ return False;
+ end if;
+
+ if L.Length = 2 then
+ if L.First.Next /= L.Last then
+ return False;
+ end if;
+
+ if L.Last.Prev /= L.First then
+ return False;
+ end if;
+
+ return True;
+ end if;
+
+ if L.First.Next = L.Last then
+ return False;
+ end if;
+
+ if L.Last.Prev = L.First then
+ return False;
+ end if;
+
+ if Position.Node = L.First then
+ return True;
+ end if;
+
+ if Position.Node = L.Last then
+ return True;
+ end if;
+
+ if Position.Node.Next = null then
+ return False;
+ end if;
+
+ if Position.Node.Prev = null then
+ return False;
+ end if;
+
+ if Position.Node.Next.Prev /= Position.Node then
+ return False;
+ end if;
+
+ if Position.Node.Prev.Next /= Position.Node then
+ return False;
+ end if;
+
+ if L.Length = 3 then
+ if L.First.Next /= Position.Node then
+ return False;
+ end if;
+
+ if L.Last.Prev /= Position.Node then
+ return False;
+ end if;
+ end if;
+
+ return True;
+ end;
+ end Vet;
+