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] Bug in Cil.datatype.Lval.Hashtbl?

Hello,

On Thu, Aug 9, 2012 at 8:31 AM, Boris Hollas
<hollas at informatik.htw-dresden.de> wrote:
> I understand that this->gear++, this->gear-- are different expressions. But
> why are the inner expressions this->gear different? How are the eids
> generated?

As mentioned in my previous mail, eid encode syntactic occurrence.
Currently, the parser essentially generates one eid per expression it
finds in the source code. However, the exact behavior is _not_
specified. The only guarantee is that two expressions with the same
eid will compare equal for Cil.compareExp. (In fact, hopefully, they
should be one single OCaml value.)

> Are the respective vids equal?

Yes. Each variable is uniquely identified by its varinfo. This is
explained in Cil_types.

>> want is given by the functions Cil.compareExp and Cil.compareLval, but
>
>
> These use ==.

Certainly not. The Cil.compareFoo functions start by comparing their
argument using ==, but this is only for speed reason. If == is not
sufficient to conclude, they perform a deep comparison, which will
return true on your two occurrences of this->gear.

> Is it possible to access the physical representation of ADTs?

I'm afraid I don't understand this question.

-- 
Boris Y.