--- layout: fc_discuss_archives title: Message 9 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?



Hello Virgile

Thanks! The inline worked perfectly

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

is there any  way to keep the conditional statements in the slice?

Cheers

Ivan.-


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

> Hello,
>
> Le 04/02/2020 à 20:46, Ivan Postolski a écrit :
> > Sorry for reviving this thread. To summarize what I've been doing is to
> > "emulate" a dynamic slicer with frama-c setting the -slevel to a very
> high
> > number. Now some of the subjects I'm analyzing contain recursion and
> frama-c
> > is failing with the following error:
> >
> >           [eva] file.c:449: User Error:  detected recursive call
> >
> > How can I maintain the "single execution path" though recursion? as I
> know
> > that the program terminates after probably a few recursive calls
> >
>
> Frama-C has the option -inline-calls <f1,...,fn> that instructs the kernel
> to inline each call to functions f1, ..., fn. If you know that the number
> of
> recursive calls has a finite bound, you can inline the recursive function
> several times, with e.g.
>
> frama-c <files.c> -inline f -then -inline f -then -inline f ... -then -eva
>
> Note that you more or less double the recursion depth that you can handle
> for each -then -inline f
>
> 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/f5ff372e/attachment.html>