--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on March 2009 ---
Jonathan-Christofer Demay a ?crit : > Oops, I forgot to tell that in this particular example, 'toto' is a > function from a library and its definition is not provided to frama-c > for the analysis, just its declaration. Ok. So, if you don't give any specification for 'toto', you can see (for instance using : frama-c/bin/viewer.opt -val test.c) that the tool generates a default specification : /*@ behavior generated: assigns \at(\result,Post) \from x, y; */ extern int toto(int x , int y ) ; which assumes that your "worst case scenario", ie. the result depends on both x and y. > That's why I want to assume a 'worst case scenario' and add all the > statements that statement 2 depends on to the dependencies of statement > 4. (because Db.Pdg.all_dpds stops at the OutRet and InCtrl nodes of > statement 2) The PDG normally use the specification of 'toto', so you don't need to compute dependencies yourself. In fact, it is quite dangerous to manipulate the results, because it probably means that the different analysis of the tool won't be based on the same assumptions. But if you _did_ have to try to do these computations, it is probably because something went wrong... So, let's try to find out want. On the file : -------------------------- int toto (int x, int y); void main (int a, int b, int c, int z, int e) { int e = 3; b += z; c = toto(b,a); c++; e = toto(c,a); } -------------------------- using the command : frama-c/bin/toplevel.byte -pdg-debug "-fct-pdg main " test.c You can have a look at the pdg links and see that the "Call2-OutRet" depend on "Call2-In1" and "Call2-In2". I tested the commands you used with the following .ml file --------------------------- open Db;; (* to print node lists *) let pp_nodes msg nodes = Format.printf "%s at ." msg ; List.iter (fun n -> Format.printf " %a at ." (!Pdg.pretty_node false) n) nodes;; let f = Globals.Functions.find_by_name "main";; let pdg = !Pdg.get f;; let stmt_4 = fst (Kernel_function.find_from_sid 4);; let nodes = !Pdg.find_simple_stmt_nodes pdg stmt_4;; let () = pp_nodes "[find_simple_stmt_node 4]" nodes;; let nodes = !Pdg.all_dpds pdg nodes;; let () = pp_nodes "[all_dpds from stmt 4]" nodes;; --------------------------- You can run it with frama-c toplevel which enables you to interactively test commands : ledit bin/toplevel.top ~/FramaCtests/demay-18mars09.c #directory "cil/src";; #use "/user/apacalet/home/FramaCtests/demay-18mars09.ml";; and you can see that you get (among others) : [Elem] 11 : b += z; which is the node that you want, don't you ? I don't know if I am clear and if it answers to your question... It seems that I don't understand what you are trying to do :-( Fell free to ask more questions, Bye. -- Anne Pacalet - INRIA - 2004, route des Lucioles BP.93 F-06902 Sophia Antipolis Cedex. Tel : +33 (0) 4 9715 5345