--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2020 ---
[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>