Pre-processing Source Code before slicing using Frama-c

Question

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.

Answer 1

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.