slice - 使用 Frama-c 切片前预处理源代码

Question

我试图将源代码与切片代码进行比较，但 frama-c 在解析时对代码进行了规范化，这使得切片代码语句与源代码语句不同。

是否可以使用 frama-c 预处理代码，以便当我使用标准对其进行切片时，可以将生成的切片语句与预处理语句进行比较？

谢谢。

Answer 1

是否可以使用 frama-c 预处理代码...</p>

是的！

用于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 ++;
  }
  …

通过将结果与prep.c.