Предварительная обработка исходного кода перед нарезкой с использованием Frama-c

Question

Я пытаюсь сравнить исходный код с нарезанным кодом, но frama-c нормализует код во время синтаксического анализа, что делает операторы нарезанного кода не идентичными операторам исходного кода.

Можно ли предварительно обработать код с использованием frama-c, чтобы при его разрезании по критерию можно было сравнить полученные результирующие операторы с предварительно обработанными операторами?

Благодарю.

Answer 1

Можно ли предварительно обрабатывать код с помощью frama-c …

Да!

использование frama-c … -print -ocode prep.c для предварительной обработки. Вот пример:

Оригинал:

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;
    …

Нормализованная версия получена с 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 ++;
  }
  …

Различия, вызванные любым преобразованием Frama-C, примененным к программе, намного легче прочитать, сравнивая результат с prep.c,