消息 "unreachable entry point" 是什么意思？

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

切片需要计算使用Value分析结果的PDG（Program Dependent Graph）。警告 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.

当Value分析遇到一个无效的属性时，就不能再继续下去了。因为此处警报来自第一条语句，所以其他所有内容都变得无法访问。无效的属性是 \valid_read(argv+2);，因为输入上下文的默认宽度是 argv 的 2。这可以通过使用选项 -context-width 3 或使用另一个不带参数的分析入口点（并使用 -main my_main 指定）来解决，定义 argc 和 argv 显式，并用它们调用真正的 main。

建议只有在检查值分析结果是否正确后才使用切片。您可以运行单独使用 -val 选项，并根据需要调整其他选项。

消息 "unreachable entry point" 是什么意思？

What does the message "unreachable entry point" mean?

frama-c

program-slicing