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?

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>