--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2017 ---
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. Le 02/11/2017 à 23:34, Jordi Adan Navarrette a écrit : > > 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 > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171106/3b49a3b9/attachment.html>