问题描述
以下面的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的过程中，我很想知道这里可能有什么通用方法。
解决方法
ACSL没有“分析'初始状态”或“入口点”的内在概念。每种分析（无论是否模块化）都有其自己的初始上下文概念。例如，WP是模块化的，因此其初始状态是当前正在分析的功能的前提。在Eva中，整个程序分析的初始状态更接近C11的“ 5.1.2.1。独立环境”，而不是“ 5.1.2.2。托管环境”，在某种意义上，尽管默认的初始函数称为main，但用户可以使用另一个函数名称覆盖它，并且初始参数由Eva的上下文概念以及相关选项（{{1}，-eva-context-depth，-eva-context-width）定义。
因此，对于您而言，设置-eva-context-valid-pointers将起作用。请注意，此选项会影响为初始状态创建的所有指针，因此，如果有多个指针参数，则可能会出现问题。
另一种解决方案是编写诸如-eva-context-valid-pointers之类的前提条件。它不会被Eva证明（仍为 Unknown ），但在分析过程中会加以考虑，从而防止发出警报。未来版本的Frama-C可能会包含一个/*@ requires \valid_read(foo); */（或类似的关键字），以便能够声明此类属性并将其视为有效。
最后，对于更复杂的情况，可能需要更复杂的初始上下文，并且有插件可以这样做，但是在开源发行版中不需要。在这种情况下通常要做的是在调用函数之前手动编写一个存根函数以创建初始状态。某些Frama-C内置函数（例如admit）可用于帮助创建此状态。初始状态的示例为available here，其中Frama_C_interval最多可以有5个任意字符串，每个字符串最多256个字符。这种基于存根的方法可提供更高的精度，例如如果您有一个复杂的结构，其中包含多个指针字段作为初始上下文，但这需要更多的精力。
requires（此处类似\valid(foo)子句的意思是：从被调用者的角度来看，它是可以假定的，因为它取决于调用者（或主要入口点的特定情况（外部世界），以确保函数的执行将在尊重前提条件的状态下开始。
但是，在您的特定情况下，有一个陷阱：出于技术原因，Eva确实会先创建一个初始上下文，然后根据前提条件将其简化。因此，您将收到requires未知的警告。
通常来说，让Eva在特定上下文中启动的通常方法是编写一个小的包装函数，可能使用Eva manual第9.2.1节中提到的内置函数。还有一些选项（在手册的6.3节中进行了描述）控制初始状态的计算方式。如果您不需要有关初始状态的过于精确的信息，则可能就足够了（例如，只需确保foo和任何其他指针有效，请使用-eva-context-valid-pointers）
最后，已经进行了从ACSL require子句生成包装函数的实验（请参见this paper），但据我所知，相应的插件不是免费提供的。