--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on February 2010 ---
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 ------------