--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] lval and lhost



Hello,

I want to identify the formal parameter that corresponds to an lval
inside a function, as in
foo(int *x) {*x = 0}
or
bar(struct S *s) {s->a = 0}.

However, a formal f has type Cil_types.varinfo while an lval l has type
Cil_types.lval, so they can't be compared. If l matches (Var vi, _),
then I assume vi and f can be tested for equality. I feel that this is
more complicated if l matches (Mem e, _). I assume that in this case
e.enode should match Lval l', so a recursive function could be used. Is
this true?

Also, how are struct S *s and s->a represented in the above example? I
assume that 
- struct S *s is a varinfo
- s->a matches (Mem e, Field (fi, NoOffset)), where e.enode matches
Lval(Var v, NoOffset), where v equals s and fi.name equals a.
-- 
Best regards,
Boris