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