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] Backward Conditioning?

  • Subject: [Frama-c-discuss] Backward Conditioning?
  • From: jnavarrette at gradcenter.cuny.edu (Jordi Adan Navarrette)
  • Date: Thu, 2 Nov 2017 22:34:12 +0000
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.

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