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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 21, Issue 3



Dear Pascal,
I have one more example code for contexst-sensitive points-to analysis.
In the following simple code, can we get a slicing results that do not
contain line 24 using Frama-C?
In my understanding, line 24 should not be included if
contexst-sensitive points-to analysis is working correctly.

------------- START test code ------------

typedef signed char s1;
typedef signed short s2;
typedef signed long s4;
typedef unsigned char u1;
typedef unsigned short u2;
typedef unsigned long u4;
typedef float f4;
typedef double f8;

s2 f(s2* s2var)
{
return *s2var;
}

void main(void)
{
s2 s2t_1;
s2 s2t_2;
s2 s2t_3;
s2 s2t_4;
s2 s2t_5;
s2 s2t_6;

s2t_1 = 1; // line 24: should not be included
s2t_2 = 2;

s2t_3 = f(&s2t_1);
s2t_4 = f(&s2t_2);

s2t_5 = s2t_3;
s2t_6 = s2t_4; // line 31: criteria
}

------------- END test code ------------