Iam trying to compare the source code with the sliced code, but frama-c normalizes the code at parsing time which makes the sliced code statements not identical to the source code statements.
Is it possible to Pre-processes the code using frama-c so that when I slice it using a criteria the resulting sliced statements can be compared to the pre-processed statements?
thanks.
Is it possible to Pre-processes the code using frama-c …
Yes!
Use frama-c … -print -ocode prep.c to pre-process. Here is an example:
Original:
static uint32_t func_1(void)
{
int64_t l_9 = 0xA9D6923607A98815LL;
int32_t *l_10 = &g_11;
int32_t *l_12 = (void*)0;
int32_t **l_13 = (void*)0;
int32_t **l_14 = &l_12;
uint16_t l_15 = 0UL;
int16_t *l_16 = &g_17;
uint16_t l_25 = 0x7847L;
uint8_t *l_36 = &g_37;
uint32_t *l_335 = &g_92;
uint32_t *l_336[2];
uint8_t *l_522 = &g_523;
int i;
for (i = 0; i < 2; i++)
l_336[i] = (void*)0;
…
Normalized version obtained with frama-c original.c -print -ocode prep.c:
static uint32_t func_1(void)
{
uint32_t __retres;
int64_t l_9;
int32_t *l_10;
int32_t *l_12;
int32_t **l_13;
int32_t **l_14;
uint16_t l_15;
int16_t *l_16;
uint16_t l_25;
uint8_t *l_36;
uint32_t *l_335;
uint32_t *l_336[2];
uint8_t *l_522;
int i;
int32_t *tmp_11;
int16_t tmp_1;
int32_t *tmp_0;
int16_t tmp;
uint8_t tmp_10;
uint8_t tmp_9;
int tmp_8;
uint8_t tmp_7;
int32_t *tmp_6;
int64_t tmp_5;
int tmp_4;
uint32_t tmp_3;
uint32_t tmp_2;
l_9 = (long long)0xA9D6923607A98815LL;
l_10 = & g_11;
l_12 = (int32_t *)((void *)0);
l_13 = (int32_t **)((void *)0);
l_14 = & l_12;
l_15 = (unsigned short)0UL;
l_16 = & g_17;
l_25 = (unsigned short)0x7847L;
l_36 = & g_37;
l_335 = & g_92;
l_522 = & g_523;
i = 0;
while (i < 2) {
l_336[i] = (uint32_t *)((void *)0);
i ++;
}
…
The differences caused by any Frama-C transformation applied to the program are much easier to read by comparing the result to prep.c.