3

以下面的 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 的方式,我很想知道这里的常用方法是什么。

4

2 回答 2

4

ACSL 没有“分析初始状态”或“入口点”的内在概念。每个分析,无论是否模块化,都有自己的初始上下文概念。例如,WP 是模块化的,因此它的初始状态是当前正在分析的函数的前提条件。在 Eva 中,整个程序分析的初始状态更接近 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(或类似的关键字),以便能够声明此类属性并将其视为有效。

最后,对于更复杂的情况,可能需要更复杂的初始上下文,并且有插件可以这样做,但在开源发行版中没有。在这种情况下,通常会手动编写一个存根函数以在调用该函数之前创建初始状态。一些 Frama-C 内置函数Frama_C_interval可用于帮助创建此状态。此处提供了一个初始状态示例,其中argv最多可包含 5 个任意字符串,每个字符串最长为 256 个字符。这种基于存根的方法提供了更高的精度,例如,如果您有一个包含多个指针字段作为初始上下文的复杂结构,但它需要更多的努力。

于 2020-10-07T12:48:58.963 回答
2

(requires在这里,类似\valid(foo)子句的确切含义是:从被调用者的角度来看,它可以假设,因为它取决于调用者(或者在主入口点的特定情况下,外部世界)保证函数的执行将在尊重前提条件的状态下开始。

但是,在您的特定情况下,有一个问题:出于技术原因,Eva 确实首先创建了一个初始上下文,然后根据前提条件减少它。requires因此,您会收到未知的警告。

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

最后,已经有从 ACSL requires 子句生成包装函数的实验(参见本文),但据我所知,相应的插件不是免费提供的。

于 2020-10-07T12:46:41.230 回答