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] Value analysis and approximaitons

  • Subject: [Frama-c-discuss] Value analysis and approximaitons
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 17 May 2010 22:54:29 +0200
  • In-reply-to: <9080ABF0152644E98BF844DBFE970AC6@gigel>
  • References: <9080ABF0152644E98BF844DBFE970AC6@gigel>
> ????Question is: how can I stop frama-c from making this approximation and
> instead to feed me the result of s ? {1; 2; 3; 4; 5; 107; 108; 110; ?}?

There are two ways:

1) You can recompile after having changed the constant 7 at the top of
file src/ai/ival.ml into something else.

Example: using 17 instead of 7:

s ? {1; 2; 3; 4; 5; 107; 108; 110; }

2) You can change your program to:
void main(void)
{
 int i;
 int s=0;
 int index=Frama_C_interval(0,7);
 /*@ assert index==0 || index==1 || index==2 || index==3 ||
   index==4 || index==5 || index==6 || index==7 ; */
 s=big.p[index];
 Frama_C_show_each_s(s);
}

and use the commandline:

bin/toplevel.byte -val t.c share/builtin.c -slevel 17

You get:
...
[value] Called Frama_C_show_each_s({1; })
[value] Called Frama_C_show_each_s({2; })
[value] Called Frama_C_show_each_s({3; })
[value] Called Frama_C_show_each_s({4; })
[value] Called Frama_C_show_each_s({5; })
[value] Called Frama_C_show_each_s({110; })
[value] Called Frama_C_show_each_s({107; })
[value] Called Frama_C_show_each_s({108; })

Note that I needed to insert the Frama_C_show_each_s call to prove
that the values of s were computed with precision. The precision is
still lost when the results are synthesized for recording, but there
are programmatic hooks to access the separate values before they are
thrown away.

Both methods have their own disadvantages:

Method 1) requires you to recompile, you can't report bugs in the
modified version, and performance is not guaranteed when you modify
the constant 7 too much. It may also work okay: it is just that we
have not tested the value analysis with large constants.

Method 2) does not require you to recompile, is officially supported,
but at this time you have little control over the repartition of the
superposed states that you allow with option -slevel. If your program
contains a lot of conditionals, the conditionals may eat all the
slevels you have the resources to throw at them.

Pascal