Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with int and integer in terms

Hello,

2012/8/2 Boris Hollas <hollas at informatik.htw-dresden.de>:
> On 02.08.2012 15:01, Virgile Prevosto wrote:
>> Which hash function are you using? You might want to try
>> Logic_utils.hash_term for your purpose (in Nitrogen,
>> Cil_datatype.Term.hash uses Hashtbl.hash, which gives different
>> results on terms that are considered equal by Cil_datatype.Term.equal,
>> which might be the cause of the issue you're seeing. This will be
>> fixed in Oxygen)
>
> How does Logic_utils.is_same_term differ from Cil_datatype.Term.equal and
> what should be used for the hashtable?
>

Basically, my suggestion above must be seen as a workaround for an
issue with Cil_datatype.Term.hash in Nitrogen. When it will be fixed
in Oxygen, you should use functions from Cil_datatype.Term.
Logic_utils functions are meant to be used in very particular
contexts. In fact,  the main (and possibly only) use case is the
merging phase at the end of elaboration when you have several source
files and thus cannot rely on vid &al to tell if two identifiers are
the same, and must switch to a comparison with the name of the
identifier. Cil_datatype operates in context where all symbols have
been merged, and thus use the relevant id field for that purpose. This
is the case for almost all Frama-C's operation, and unless you have a
very peculiar need (or there is a bug in Cil_datatype ;-), you should
stick with that.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile