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