--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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.

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>