SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:issue:194 [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:issue:194

how to help value analysis better understand annotations

We start with the following code, similar to the one in issue ~~Mantis:194~~

#include "/usr/share/frama-c/builtin.h"
int v = 0;
 
int v1, v2, v3, v4;
 
/*@ requires (((v1 && !(v2 && v3) && v4); */
extern void fun(void)
{
  if (v1) {
      if (v4) {
          if (v2) {
            if(v3) {v++;}
          }
      }
   }
  return v;
}
 
int main() {
  v1 = Frama_C_nondet(0,1);
  v2 = Frama_C_nondet(0,1);
  v3 = Frama_C_nondet(0,1);
  v4 = Frama_C_nondet(0,1);
  fun(); return 0; }

if we try to slice calls to fun, with

frama-c -slice-calls fun slicing.c -slice-print

we see that the slicer do not remove the v++ instruction, although a little reasoning can show us that the pre-condition of fun implies that the code is never executed.

The issue lies with the interpretation of the pre-condition by the value analysis. When it encounters an annotation whose validity can not be decided, it tries to reduce its current state by eliminating the values that are incompatible with the annotation. However, this does not always succeed. In fact, value analysis uses abstract state, and the abstraction may not be precise enough to represent the reduced state. For instance, if we know that -10 ⇐ x ⇐ 10, the assertion x != 0 won't help us, since possible variable values are represented by an interval1), and the only interval that can represent all values between -10 and -1 or 1 and 10 is still [-10;10]. Thus, in our example, it would be better if the vi were known to be real booleans (i.e. to be either 0 or 1), which in the example can be achieved by adding $FRAMAC_SHARE/builtin.c on the command line, since it contains the code for Frama_C_nondet. In this case v1 != 0 implies v1=12).

Moreover, logical connectors tend to confuse the value analysis: it is better to write several small annotations than a big one. In the same vein, assert present a few advantages over requires: when using the -slevel option, an assert with a disjunction will lead to separate states (one for each of the member of disjunction, in the limit given by -slevel argument), which will be analyzed independently, leading to more precise results: in our example, rewriting the pre-condition !(v2 && v3) as an assertion !v2 || !v3 and using -slevel 2 will lead to two separate analyses, one in which v2 is known to be 0 (while v3 is still unknown), and one in which v3 is equal to 0 while v2 is unknown. This is sufficient for the value analysis to detect that v++ is unreachable and thus to obtain the desired slice.

To sum up, with the following (equivalent to the original) annotated code

#include "/localhome/virgile/Frama-C/share/builtin.h"
int v = 0;
 
int v1, v2, v3, v4;
 
extern void fun(void)
{
  /*@ assert v1; */
  /*@ assert !v2 || !v3; */
  /*@ assert v4; */
  if (v1) {
      if (v4) {
          if (v2) {
            if(v3) {v++;}
          }
      }
   }
  return v;
}
 
int main() {
  v1 = Frama_C_nondet(0,1);
  v2 = Frama_C_nondet(0,1);
  v3 = Frama_C_nondet(0,1);
  v4 = Frama_C_nondet(0,1);
  fun(); return 0; }

and the command line

frama-c -slice-calls fun slicing.c /usr/share/frama-c/builtin.c -slice-print -slevel 2

we obtain the desired result:

extern void fun_slice_1(void) 
{ 
 
  return;
 
}
void main(void) 
{ 
 
  {fun_slice_1();
  return;}
 
}
1)
the real representation is slightly more sophisticated, but for the purpose of the example, we can stick to that
2)
it would be sufficient that 0 is a bound of the interval, e.g v1>=0
mantis/frama-c/issue/194.txt · Last modified: 2009/07/17 17:36 by virgile