Qstack
Mutable stack in which it is possible to add data at the end (like a queue) and to handle non top elements. Current implementation is double linked list.
module type DATA = sig ... end
module Make (D : DATA) : sig ... end
Frama-C