--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Understanding slicing results



Pascal Cuoq wrote :
> We will look at the behavior you have reported.
>   
The loose of precision comes from the computed PDG of fonction f.
It merge all calling context. The following command line in Beryllium
20090902 gives the graphical representation in file f.f.dot :
   frama-c -lib-entry t.c -calldeps -val -dot-pdg f -pdg

In this PDG, s2t_1 appears as an input. The spare mark attributed
to that data comes from the inter-procedural slicing computation
which relies on context-sensitive information at the call site,
and merged information for the PDG of the called function.

This problem is well known. It requires a lot of modifications to solve it
and this kind of /imprecision/ (attribution of a spare mark which means:
/do no impact slicing criteria/ ) isn't so critical since plugings 
developped
over the slicing pluging can retrieve this mark (the GUI does).

Patrick.

-- 
Patrick Baudin,
CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100211/fe7f0291/attachment-0001.htm 
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: f_pdg.png
Type: image/png
Taille: 28052 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100211/fe7f0291/attachment-0001.png