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] dead code while trying to slice
- Subject: [Frama-c-discuss] dead code while trying to slice
- From: prubel at bbn.com (Paul Rubel)
- Date: Wed, 10 Oct 2012 17:31:25 -0400
I'm new to frama-c and after reading through the value analysis manual and trying a few example programs I though I'd dive into slicing some non-trivial code, specifically openssh-6.1p1. I've been having a hard time of it and am hoping someone can provide some guidance. Initially I needed to turn off analysis of recursive functions. I'm aware that this leads to unsoundness but I was hoping that the results might be better than nothing. Running frama-c gives me ~400 assertion warnings along with a lot of "No code for function ... default assigns generated". If I push on and try to slice nearly all of the code is marked as unreachable (with a red line through it), including the function I want to slice. Do I need to address all the assertions, which are marked as warnings, before I can expect a reasonable slice or am I already completely out of luck due to the recursion flag? At a higher level, how do folks go about debugging too much code being marked as dead when trying to slice? Are there certain messages or types of messages that I should be particularly looking for or flags that would be helpful? I've tried the GUI as well as the commandline with the following: frama-c -slice-pragma ssh_local_cmd -val-ignore-recursive-calls *.i Thank you for your help, Paul
- Follow-Ups:
- [Frama-c-discuss] dead code while trying to slice
- From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
- [Frama-c-discuss] dead code while trying to slice
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] dead code while trying to slice
- Prev by Date: [Frama-c-discuss] Problem with Jessie and float division
- Next by Date: [Frama-c-discuss] dead code while trying to slice
- Previous by thread: [Frama-c-discuss] Problem with Jessie and float division
- Next by thread: [Frama-c-discuss] dead code while trying to slice
- Index(es):