使用Frama-c

Question

在切片之前預處理源代碼Iam嘗試將源代碼與切片代碼進行比較，但frama-c在解析時對代碼進行規範化，這使得切片代碼語句與源代碼語句不相同。

是否有可能使用frama-c預處理代碼，以便在使用條件對其進行切片時，可以將生成的切片語句與預處理語句進行比較？

謝謝。

Answer 1

是否有可能使用郵資-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 ++; 
    } 
    … 

由施加到該程序的任何郵資-C轉化的差異是更容易閱讀通過將結果與prep.c進行比較。