--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on August 2012 ---
[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.