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,

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