--- layout: fc_discuss_archives title: Message 8 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,

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