--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2012 ---
Hello, Before using slicing, you have to be satisfy with the results of the value analysis (the slicing relies on it). That means you have to a look at the assigns generated for functions without code since these assigns are used as hypothesis of your analysis. For the slicing analysis, you have to gives in addition to the assigned memory locations, correct dependencies between these locations and their inputs for all functions without code. So you have to look again at these generated assigns clauses, more carefully. Incorrect assigns locations or incorrect assigns dependencies give incorrect slices. The dead code information is directly a result of the value analysis. Trying to understand why some code is dead with the slicing analysis needs more inputs from you than in using only the value analysis. Patrick. Le 10/10/2012 23:31, Paul Rubel wrote : > 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 > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > . >