Frama-C-discuss mailing list archives

jnavarrette at gradcenter.cuny.edu (Jordi Adan Navarrette) · Mon, 15 Jan 2018 22:15:57 +0000

In an early inquiry, I expressed an understanding that conditioned slicing could be done by using assertions (also, requires statements) along with one of the slicing options. In Conditioned Program Slicing (Canfora, Cimitile, De Lucia, 1998), the authors present the following example (modified for use in Frama-C), demonstrating the occurrence of overly-conservative slices that result from using static dependencies:

int f(int a, int x, int y) {

  //@ assert a > 0;

  int z;

  x = y + 2;

  if (a > 0)

    x = y * 2;

  z = x + 1;

  return z;

}

Slicing with respect to the return value of f yields the following "conditioned slice":

int f(int x, int y) {

  int z;

  x = y + 2;

  x = y * 2;

  z = x + 1;

  return z;

}

As noted in the paper, and can be easily observed, the first assignment to x should be eliminated. Consider the following expansion on that problem:

int f(int a, int x, int y) {

  //@ assert A && (!A || B) && (!(A && B) || C);

  int z;

  x = y + 2;

  if (A) { x = y * 2;

    if (B) { x = y / 2;

      if (C) { x = y - 2;}

    }

  }

  z = x + 1;

  return z;

}

If A is (a > 0), B is (x > 0) and C is (y > 0), then the conditionals are removed but the assignments all remain. It is worth mentioning that slicing again wrt the return value gives the correct slice, but are there any options or features that allow this to be computer correctly after one application of "conditioned slicing"?

If A is (a > 0), B is (a%2 > 0) and C is (a%3 > 0), then only the first conditional is removed, and not only does the assignment still remain, but the complete assertion as well. Any repeated applications of "conditioned slicing" don't reduce the program further. It is worth mentioning that if we assert a == 7, all the conditionals go away, leaving all the assignments still to be sliced after another application, but I ask again, are there any options or features that allow this to be computed correctly after one application?

Thanks in advance.

________________________________
From: BAUDIN Patrick <Patrick.Baudin at cea.fr>
Sent: Monday, November 6, 2017 2:15:13 AM
To: frama-c-discuss at lists.gforge.inria.fr
Cc: Jordi Adan Navarrette
Subject: Re: [Frama-c-discuss] Backward Conditioning?

The Slicing plug-in of Frama-c does not support backward conditioning (the plug-in relies on the Value Analysis plugin which performs only forward propagation of ACSL conditions).

-- Patrick Baudin.

Backward conditioning (Fox, Harman, Hierons, Danicic, 2001) is a slicing method that is intended to elide statements from a program that cannot lead to the satisfaction of a condition being asserted later in the program, whereas conditioned program slicing  (aka "forward conditioning") is meant to eliminate statements that would never be executed if a condition on the input variables is to be satisfied. (For the purpose of this question, I am ignoring entirely the statement and variables in the criterion.)

I understand that more "generalized" conditioned program slicing can be achieved by inserting assertions where desired so that those statements that are not reachable thereafter are eliminated (sparecode), leaving what remains for slicing. I understand that forward slicing is carried out by impact, and that backward slicing is carried out by slicing, but forward vs backward slicing is unrelated to forward vs. backward conditioning.

Does Frama-C currently support backward conditioning? Thanks in advance.

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180115/9db70dc5/attachment-0001.html>