--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2017 ---
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>