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] frama-c "dynamic" slicing?

Hi Virgile

Okay, that makes sense, thanks anyway!

On Wed, Feb 5, 2020 at 4:16 PM Virgile Prevosto <virgile.prevosto at m4x.org>
wrote:

> Hello,
>
> Le mer. 5 févr. 2020 à 18:40, Ivan Postolski <ivan.postolski at gmail.com> a
> écrit :
>
>>
>> Now I'm having another curious behaviour with the same slicing mode, if I
>> have a code like the following:
>>
>> foo(int x) {
>>      if (x > 5) {
>>           y = x ;
>>      } else {
>>           y = 2*x;
>>      }
>>     return y; //<- slicing criteria
>> }
>>
>> then executing one branch of foo, the if-else condition is not kept in
>> the frama-c slice
>>
>> for instance
>>
>> main() {
>>      foo(6);
>> }
>>
>> will only keep the y=x, return y;
>>
>> or
>>
>> main() {
>>      foo(3);
>> }
>>
>> will keep the y=2*x return y;
>>
>> and discard the conditional statements from the slice
>>
>>
> I'm afraid this is unavoidable: the analysis is **too** precise, and the
> slicing detects that in this context the test is always true (or false), so
> that it does not really have an effect on the value of y at return point. A
> quite ugly workaround would be to slightly modify the test so that it has a
> side-effect, and ask for the slicing to keep it as well:
>
> int y;
>
> int foo(int x) {
>      int if1;
>      /*@ slice pragma stmt; */
>      if (if1 = x > 5) {
>           y = x ;
>      } else {
>           y = 2*x;
>      }
>     /*@ slice pragma stmt; */
>     return y; //<- slicing criteria
> }
>
>
> int main() {
>      foo(6);
> }
>
> gets you (frama-c -eva-precision 11 -slice-pragma foo file.c -then-last
> -print)
>
> /* Generated by Frama-C */
> int y;
> int foo_slice_1(int x)
> {
>   int if1;
>   /*@ slice pragma stmt; */
>   {
>     if1 = x > 5;
>     if (if1) y = x;
>   }
>   /*@ slice pragma stmt; */
>   return y;
> }
>
> void main(void)
> {
>   foo_slice_1(6);
>   return;
> }
>
> If you know OCaml, writing a script to convince Frama-C to add a local
> variable, the pragma and the assignment for each if in the program should
> be doable.
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta
> Virgile
> _______________________________________________
> Frama-c-discuss mailing list
> 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/20200205/4c43010c/attachment-0001.html>