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

[Frama-c-discuss] on context sensitive points-to analysis



There is an example where a statement gets a spare mark and
cannot be removed. Othewise, the execution of the sliced code
will crash !

The command line is:
frama-c-gui spare_mark.c -slice-return g -lib-entry -main g

int X, Y ;
void f(int x, int y)
{
X += x ;
Y = 100/y ;
}

int U, V ;
int g(int val)
{
V = 0 ;
X = V ;
V = val ; // <- statement with a spare mark
f(U, V);
f(V, X);
return Y;
}

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