# 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*: Mon, 15 Jan 2018 22:15:57 +0000*In-reply-to*: <2103b191-2408-402b-5668-964ca34d9072@cea.fr>*References*: <CY4PR11MB1318CFADA472B0AD14E738F9E65C0@CY4PR11MB1318.namprd11.prod.outlook.com>, <2103b191-2408-402b-5668-964ca34d9072@cea.fr>

In an early inquiry, I expressed an understanding that conditioned slicing could be done by using assertions (also, requires statements) along with one of the slicing options. In Conditioned Program Slicing (Canfora, Cimitile, De Lucia, 1998), the authors present the following example (modified for use in Frama-C), demonstrating the occurrence of overly-conservative slices that result from using static dependencies: int f(int a, int x, int y) { //@ assert a > 0; int z; x = y + 2; if (a > 0) x = y * 2; z = x + 1; return z; } Slicing with respect to the return value of f yields the following "conditioned slice": int f(int x, int y) { int z; x = y + 2; x = y * 2; z = x + 1; return z; } As noted in the paper, and can be easily observed, the first assignment to x should be eliminated. Consider the following expansion on that problem: int f(int a, int x, int y) { //@ assert A && (!A || B) && (!(A && B) || C); int z; x = y + 2; if (A) { x = y * 2; if (B) { x = y / 2; if (C) { x = y - 2;} } } z = x + 1; return z; } If A is (a > 0), B is (x > 0) and C is (y > 0), then the conditionals are removed but the assignments all remain. It is worth mentioning that slicing again wrt the return value gives the correct slice, but are there any options or features that allow this to be computer correctly after one application of "conditioned slicing"? If A is (a > 0), B is (a%2 > 0) and C is (a%3 > 0), then only the first conditional is removed, and not only does the assignment still remain, but the complete assertion as well. Any repeated applications of "conditioned slicing" don't reduce the program further. It is worth mentioning that if we assert a == 7, all the conditionals go away, leaving all the assignments still to be sliced after another application, but I ask again, are there any options or features that allow this to be computed correctly after one application? Thanks in advance. ________________________________ From: BAUDIN Patrick <Patrick.Baudin at cea.fr> Sent: Monday, November 6, 2017 2:15:13 AM To: frama-c-discuss at lists.gforge.inria.fr Cc: Jordi Adan Navarrette Subject: Re: [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<mailto:Frama-c-discuss at lists.gforge.inria.fr> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180115/9db70dc5/attachment-0001.html>

- Prev by Date:
**[Frama-c-discuss] JFLA 2018 : dernier appel à participation** - Next by Date:
**[Frama-c-discuss] Frama-C Slicing Issues** - Previous by thread:
**[Frama-c-discuss] JFLA 2018 : dernier appel à participation** - Next by thread:
**[Frama-c-discuss] Frama-C Slicing Issues** - Index(es):