Hi,

Le 14/10/2013 17:30, Enrico Tassi a écrit :
> let collect k = HT.remove values !k
> 
> (* The only reference to the boxed key is the one returned, when the user drops
>    it the value eventually disappears from the values table above *)
> let create (v : 'a) : 'a key =
>   let k = mk_key () in
>   HT.add values !k (Obj.repr v);
>   Gc.finalise collect k;
>   k


In that piece of code, you should take care to the fact that the
finalizer can be called at /any/ moment.

In particular, it can be called while you are modifying your hash table.
If this situation happens, then you are modifying the hash table (by
removing elements) when it is in an unconsistent state.

Did you think about that ? Do I miss something ?

The authors of Why3 encountered similar problems. I suggest you to read
the Weakhtbl module, that gives a solution to this problem.

Regards,
-- 
Jacques-Henri Jourdan