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: jsdslml at gmail.com (jsd slml)
  • Date: Fri, 16 Jan 2009 16:54:34 +0100
  • In-reply-to: <5EFD4D7AC6265F4D9D3A849CEA9219191AB120@LAXA.intra.cea.fr>
  • References: <5EFD4D7AC6265F4D9D3A849CEA9219191AB11D@LAXA.intra.cea.fr> <bacfeaa40811280930r1b6f0e46xad400ebefbdf4646@mail.gmail.com> <5EFD4D7AC6265F4D9D3A849CEA9219191AB120@LAXA.intra.cea.fr>
Hi,

I kept playing with frama-c's source code and now it's a bit easier for me
to do what I have in mind, however I still haven't really figured out how to
use the slevel option from the value analyzis plugin.

For now, this is how I retrieve the variation domain of a list of variables
at a particular instruction in the project (I'm not sure it's the proper way
to do it).

for i = 0 to ((List.length vars_list) - 1) do
  match (List.nth vars_list i) with
  | Lval(lv) ->
    let offsetmap_b = !Db.Value.lval_to_offsetmap
~with_alarms:CilE.warn_none_mode ki lv in
    Format.printf "%s" (fprintf_to_string "'%a'" (self#pretty_offsetmap lv)
offsetmap_b);
  | _ ->

(pretty_offsetmap being ripped off from value/register_gui.ml, ki being the
current stmt in the visitor)

Now, I would like to retrieve as for the variation domain of this list,
still at a particular instruction in the project, a set of t-uples, does
someone have any hint on how to do this ? I know that (List.length
vars_list) will be limited by SemanticUnrollingLevel, but couldn't find in
the source code how to ask for that.

Regards

On Mon, Dec 1, 2008 at 5:01 PM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote:

> If what you are really interested in is a set of tuples of possible values
> for the variables of the program, you can have this with the -slevel
> option of the value analysis. But note that when the value analysis
> gives you the set {(0,1,1),(1,0,1)}, it neither guarantees that there
> are at least two different paths (one of the tuples could correspond
> to a path that is in fact not feasible at all), nor that there are at most
> two different paths. On the following example
>
> if (complex condition)
> {
>  y =1
>  x = 2;
> }
> else
> {
>  x = 2;
>  y = 1;
> }
>
> the analyzer will provide the (2,1) tuple for (x,y) only once, although
> this value can be obtained through two different paths. This is
> because the analyzer systematically checks if a tuple (say, the tuple
> coming
> from the else branch) is included in the tuples it already has
> (the tuple for the then branch). This inclusion check is also how
> the analyzer may give correct results for a loop
> that takes 1000 iterations at run time
> (or even a loop that does not obviously terminate)
> without running through the body of the loop 1000 times.
>
> The guarantee is that each possible path at run-time gives a
> (so-called "concrete") tuple of values
> that is included in at least one of the "abstract" tuples
> computed by the analyzer.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090116/7d140a3a/attachment.htm