Le 7 déc. 07 à 20:54, Jean-Christophe Filliâtre a écrit :

> forum@x9c.fr a écrit :
>>> Indeed. However, note that it uses internally a hash table to store
>>> blocks already considered (in order to correctly account for  
>>> sharing),
>>> and thus it is potentially incorrect if the GC moves some blocks  
>>> during
>>> the count, for instance during a resizing of the hash table (which
>>> triggers the GC). I don't know how to avoid this issue; any help  
>>> is welcome.
>>
>> Sorry for the noise but doesn't this mean that the "size" function  
>> may not
>> terminate ?
>
> No, simply that it may count a same block several times, because it  
> was
> moved by the GC during a resizing of the hash table, between the first
> time it was seen and the next time it is reached from another block.
>
> So you may only overestimate the size of the data. It should not fail,
> and should terminate, even on cyclic values.

My mistake, I did not take into account the fact that if a block is  
moved by the
garbage collector, its reference is updated in the hashtable *too*.
Hence the termination guarantee.