--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2009 ---
Hi, I kept playing with frama-c's source code and now it's a bit easier for me to do what I have in mind, however I still haven't really figured out how to use the slevel option from the value analyzis plugin. For now, this is how I retrieve the variation domain of a list of variables at a particular instruction in the project (I'm not sure it's the proper way to do it). for i = 0 to ((List.length vars_list) - 1) do match (List.nth vars_list i) with | Lval(lv) -> let offsetmap_b = !Db.Value.lval_to_offsetmap ~with_alarms:CilE.warn_none_mode ki lv in Format.printf "%s" (fprintf_to_string "'%a'" (self#pretty_offsetmap lv) offsetmap_b); | _ -> (pretty_offsetmap being ripped off from value/register_gui.ml, ki being the current stmt in the visitor) Now, I would like to retrieve as for the variation domain of this list, still at a particular instruction in the project, a set of t-uples, does someone have any hint on how to do this ? I know that (List.length vars_list) will be limited by SemanticUnrollingLevel, but couldn't find in the source code how to ask for that. Regards On Mon, Dec 1, 2008 at 5:01 PM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote: > If what you are really interested in is a set of tuples of possible values > for the variables of the program, you can have this with the -slevel > option of the value analysis. But note that when the value analysis > gives you the set {(0,1,1),(1,0,1)}, it neither guarantees that there > are at least two different paths (one of the tuples could correspond > to a path that is in fact not feasible at all), nor that there are at most > two different paths. On the following example > > if (complex condition) > { > y =1 > x = 2; > } > else > { > x = 2; > y = 1; > } > > the analyzer will provide the (2,1) tuple for (x,y) only once, although > this value can be obtained through two different paths. This is > because the analyzer systematically checks if a tuple (say, the tuple > coming > from the else branch) is included in the tuples it already has > (the tuple for the then branch). This inclusion check is also how > the analyzer may give correct results for a loop > that takes 1000 iterations at run time > (or even a loop that does not obviously terminate) > without running through the body of the loop 1000 times. > > The guarantee is that each possible path at run-time gives a > (so-called "concrete") tuple of values > that is included in at least one of the "abstract" tuples > computed by the analyzer. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090116/7d140a3a/attachment.htm