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] Use Frama-C to dump all read and write memory accesses in a given C program

On 11/10/16 14:45, s.darabi at utwente.nl wrote:
> In particular, I need to know all
> the read or write memory accesses in a given C program. Do you think I
> can use Frama-C for that purpose? if yes, can you give me some hints
> about how to do it?

Yes, Frama-C is a very good fit for this. To collect memory accesses, 
you would write a visitor that traverses the AST and looks for the nodes 
that interest you. See the plugin development guide at 
http://frama-c.com/download/frama-c-plugin-development-guide.pdf for how 
to write simple visitors.

For the format of the AST, see doc/code/html/Cil_types.html in your 
Frama-C distribution (you might have to "make doc" first).

In the AST, all forms of pointer-based accesses to objects (*p, p->foo, 
p[i] when p is a pointer) are represented by lvalues of the form

     (Mem exp, offset)

where exp is the expression that is being dereferenced. Further, the AST 
is normalized by adding extra assignment statements to ensure that 
expressions have no side effects. For example, the statement

     a = b++ - c++;

is represented as something like

     tmp = b;
     b ++;
     tmp_0 = c;
     c ++;
     a = tmp - tmp_0;

So, to a first approximation, you can find all pointer-based reads by 
looking for expressions of the form

     Lval (Mem exp, offset)

and all pointer-based writes by looking for assignment statements (with 
the constructor Set) of the form

     Set ((Mem exp, offset), rhs_exp, location)

You can then extend this to handle function calls, which are normalized 
in a similar way.

Finally, you should keep in mind that "memory accesses" are not 
necessarily the same thing as accesses through pointers at the C level. 
You will have to define precisely for yourself what constitutes a 
"memory access". In particular, you will probably want to treat accesses 
to global variables as "memory accesses" even though they are not of the 
form (Mem _, _) in Frama-C but rather (Var vi, _) where vi.vglob is true.

I hope this helps!


Gergö