--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] dead code while trying to slice



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