消息「無法訪問的入口點」是什麼意思？

Question

我有一個包含文件數ACSL斷言（file.c）：

#include <stdio.h> 
#include <stdlib.h> 

void foo() { 
    int a=0; 
    //@ assert(a==0); 
} 

void print(const char* text) { 
    int a=0; 
    //@ assert(a==0); 
    printf("%s\n",text); 
} 

int main (int argc, const char* argv[]) { 
    const char* a1 = argv[2]; 

    print(a1); 
    foo(); 

    if (!a1) 
     //@ assert(!a1); 
     return 0; 
    else 
     return 1; 
} 

我想切片用命令所有斷言：

frama-c -slice-assert @all file.c -then-on 'Slicing export' -print -ocode slice.c 

然而，切片看起來並不如預期（以其實它不包含文件中包含的任何功能）：

/* Generated by Frama-C */ 
typedef unsigned int size_t; 
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */ 

/*@ 
axiomatic dynamic_allocation { 
    predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status; 

    } 
*/ 
void main(void) 
{ 
    char const *a1; 
    return; 
} 

而是我得到這樣的輸出：

file.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+2); 
[value] Recording results for main 
[value] done for function main 
file.c:16:[value] Assertion 'Value,mem_access' got final status invalid. 
[slicing] making slicing project 'Slicing'... 
[slicing] interpreting slicing requests from the command line... 
[pdg] computing for function foo 
[pdg] warning: unreachable entry point (sid:1, function foo) 
[pdg] Bottom for function foo 
[slicing] bottom PDG for function 'foo': ignore selection 
[pdg] computing for function main 
file.c:21:[pdg] warning: no final state. Probably unreachable... 
[pdg] done for function main 
[pdg] computing for function print 
[pdg] warning: unreachable entry point (sid:5, function print) 
[pdg] Bottom for function print 
[slicing] bottom PDG for function 'print': ignore selection 

它打算什麼錯在這裏，特別是有哪些呢unreachable entry point？觀察：如果我將argv[2]更改爲argv[1]，我沒有這些問題（但仍在第一行中收到警告）。

Answer 1

切片需要計算使用值分析結果的PDG（程序相關圖）。警告unreachable entry point意味着，在您給出的上下文中，函數foo不可訪問（即，它是由不可訪問的語句調用的）。

很難告訴你更多沒有一個例子...

---

編輯：

在您提供的輸出中，注意行：

file.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+2); 

和

file.c:16:[value] Assertion 'Value,mem_access' got final status invalid. 

當價值分析遇到一個無效的財產時，它不能再走下去。因爲這裏的警報來自第一條語句，所有其他的東西都變得無法訪問。無效屬性爲\valid_read(argv+2);，因爲輸入上下文的默認寬度爲argv。這可以通過使用選項-context-width 3或通過使用另一個不帶參數的分析入口點（並指定它與-main my_main）來固定，請明確定義argc和argv，並用它們調用真正的main。

建議只有在檢查了值分析結果是否正確後才能使用切片。您可以使用-val選項單獨運行，並根據需要調整其他選項。