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] 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