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] Getting a node from its id for a particular pdg

  • Subject: [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
  • Date: Fri, 20 Mar 2009 10:23:48 +0100
  • In-reply-to: <1237402185.3508.226.camel@supelec>
  • References: <1237387890.3508.114.camel@supelec> <49C116F4.5050507@sophia.inria.fr> <1237402185.3508.226.camel@supelec>
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