您如何告诉 Frama-C 和 Eva 入口点的参数被假定为有效？

Question

以下面的C代码为例。

struct foo_t {
    int bar;
};

int my_entry_point(const struct foo_t *foo) {
    return foo->bar;
}

在我们的例子中，my_entry_point 将从程序集调用，并且必须假设这里的 *foo 始终是正确的。

运行命令行...

frama-c -eva -report -report-classify -report-unclassified-warning ERROR -c11 -main my_entry_point /tmp/test.c

...结果...

[report] Monitoring events
[kernel] Parsing /tmp/override.c (with preprocessing)
[eva] Analyzing a complete application starting at my_entry_point
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva:alarm] /tmp/override.c:6: Warning:
  out of bounds read. assert \valid_read(&foo->bar);
[eva] done for function my_entry_point
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function my_entry_point:
  __retres ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  1 function analyzed (out of 1): 100% coverage.
  In this function, 2 statements reached (out of 2): 100% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  1 alarm generated by the analysis:
       1 invalid memory access
  ----------------------------------------------------------------------------
  No logical properties have been reached by the analysis.
  ----------------------------------------------------------------------------
[report] Classification
[ERROR:eva.unclassified.warning] Unclassified Warning (Plugin 'eva')
[REVIEW:unclassified.unknown] my_entry_point_assert_Eva_mem_access
[report] Reviews     :    1
[report] Errors      :    1
[report] Unclassified:    2
[report] User Error: Classified errors found
[kernel] Plug-in report aborted: invalid user input.

当然，我们总是可以添加一个基本案例 NULL 检查，它满足检查器的要求（无论如何，这可能是我们现在解决这个问题的方法）。

if (!foo) return 0;

但我更好奇（出于学习目的）如何使用例如ACSL 注释告诉检查器“嘿，我们知道这是指针，理论上可能是无效的 - 但是，请假设，因为它是入口点，所以它确实有效”。

这是 ACSL 支持的东西吗，或者可以通过 frama-c 的命令行参数改变行为吗？我明白为什么标准委员会可能对向 ACSL 添加这样的机制犹豫不决，因为它可能会被滥用，但鉴于我只是在学习 ACSL，我很想知道这里的通用方法是什么。

Answer 1

requires（这里，类似于 \valid(foo) 子句的意思恰恰是：从被调用者的角度来看，这是它可以假设的东西，因为它取决于调用者（或者在主入口点的特定情况下，外部世界）以保证函数的执行将在尊重 pre-condition.

的状态下开始

但是，在您的特定情况下，有一个问题：出于技术原因，Eva 会先创建一个初始上下文，然后根据 pre-condition 减少它。因此，您会收到 requires 未知的警告。

一般来说，让Eva在特定上下文中启动的通常方法是编写一个小的包装函数，可能会使用Eva manual的9.2.1节中提到的built-ins。还有一些选项（在手册的第 6.3 节中描述）控制初始状态的计算方式。如果您不需要关于初始状态的过于精确的信息，它们可能就足够了（例如，只需确保 foo 和任何其他指针有效，使用 -eva-context-valid-pointers）

最后，已经有关于从 ACSL requires 子句生成包装函数的实验（参见 this paper），但据我所知，相应的 plug-in 不是免费提供的。

Answer 2

ACSL 没有“分析的初始状态”或“入口点”的内在概念。每个分析，无论是否模块化，都有其自己的初始上下文概念。例如，WP 是模块化的，它的初始状态是当前正在分析的函数的前提条件。在 Eva 中，whole-program 分析的初始状态更接近于 C11 的“5.1.2.1. 独立环境”而不是“5.1.2.2. 托管环境”，在这个意义上，虽然默认的初始函数称为 main，用户可以用另一个函数名覆盖它，初始参数由 Eva 的上下文概念定义，并带有相关选项（-eva-context-depth、-eva-context-width、-eva-context-valid-pointers）。

因此，在您的情况下，设置 -eva-context-valid-pointers 会起作用。请注意，此选项会影响为初始状态创建的所有指针，因此如果有多个指针参数，则可能会出现问题。

另一种解决方案是写一个前提条件，例如/*@ requires \valid_read(foo); */。它不会被 Eva 证明（它将保持 Unknown），但在分析过程中会考虑到它，从而防止发出警报。 Frama-C 的未来版本可能包含一个 admit（或类似关键字），以便能够说明此类属性并将其视为有效。

最后，对于更复杂的情况，可能需要更复杂的初始上下文，plug-ins 可以这样做，但 open-source 分布中没有。在这种情况下通常做的是手动编写存根函数以在调用函数之前创建初始状态。可以使用一些 Frama-C built-in 函数，例如 Frama_C_interval 来帮助创建此状态。初始状态的一个例子是 available here，其中 argv 最多可以有 5 个任意字符串，每个字符串最多 256 个字符长。这种 stub-based 方法提供了更高的精度，例如如果你有一个包含多个指针字段作为初始上下文的复杂结构，但它需要更多的努力。

您如何告诉 Frama-C 和 Eva 入口点的参数被假定为有效？

How do you tell Frama-C and Eva that an entry point's parameters are assumed valid?

c

frama-c

acsl