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?

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>