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

プログラムに適用された Frama-C 変換によって生じる違いは、結果を と比較することで、はるかに読みやすくなりますprep.c。