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] interfacing non-OCaml programs with Frama-C

  • Subject: [Frama-c-discuss] interfacing non-OCaml programs with Frama-C
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Mon, 2 Feb 2009 18:28:47 +0100
  • In-reply-to: <bacfeaa40902020604j1a3283fbl42670a8efb54ccf1@mail.gmail.com>
  • References: <5EFD4D7AC6265F4D9D3A849CEA9219191AB11D@LAXA.intra.cea.fr> <bacfeaa40811280930r1b6f0e46xad400ebefbdf4646@mail.gmail.com> <5EFD4D7AC6265F4D9D3A849CEA9219191AB120@LAXA.intra.cea.fr> <bacfeaa40901160754h432d2715u5627b90af7080e57@mail.gmail.com> <5EFD4D7AC6265F4D9D3A849CEA9219191AB147@LAXA.intra.cea.fr> <bacfeaa40901200424j11629bf0p776b0d151f6bf13@mail.gmail.com> <E9D16C7B-8990-467A-9378-CEDC56EF5956@cea.fr> <73386FB2-7D76-43BF-8C79-D284F0CC1977@cea.fr> <bacfeaa40902020604j1a3283fbl42670a8efb54ccf1@mail.gmail.com>
On Feb 2, 2009, at 3:04 PM, jsd slml wrote:
>
> I have a question about this Locations.Zone.t option
>
> for example, with this code:
>
> int a, b;
> void dummy(int,int);
>
> void main(int c){
>
>     c = c ? 0 : 1;
>     if (c)
>         b = 2;
>     a = c;
>
>     dummy(a,b);
> }
>
> While visiting this code, at the instruction that call dummy, can  
> this tell me that lval 'a' depends on 'c' ? can it tell for lval 'b' ?

No.

The dependencies optionally computed by passing an argument of
the kind "Some zone" are only one of the building blocks necessary
for the dependencies that you are asking for. The dependency of
an lvalue such as "c" is nothing. The dependency of an l-value such
as "t[a+b]" is made of "a" and "b" (assuming t is an array).

The dependencies that you want seem to correspond exactly to
those computed by option -deps or -calldeps, which are computed
at every statement of the function even though they are only displayed
for the last one. Both options are implemented
in the same plug-in src/from.
I already recommended you take look at these options in
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-December/000251.html
I invite you to read this message again with the experience
you have accumulated since. Do not hesitate to look at the
implementation of this plug-in if these options are exactly
what you want, except that you need the dependencies in at
another statement than the last one.

If these dependencies do not do what you want for some reason,
it would be better to give an explanation of how they do not
accomplish what you want, rather than asking for a (lengthy)
discussion on how you can write a plug-in that computes
identical dependencies.

> If that's the case, I'm not sure what I need to pass as the 'deps'  
> argument, and how to process the first component of the returned  
> couple.
> In the end, I would like to have a list of lval (or exp) on which  
> the lval given to eval_lval depends, so I can also evaluate them.


You can activate the computation of path dependencies
by passing "(Some Locations.Zone.bottom)".
You obtain a zone, which is an abstract representation for
a set of bits in memory. Zones can not in general be
transformed into l-values (in the presence of unions or casts
in the program, the l-value may not exist at all).

Pascal