- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
以下面的 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 的上下文概念定义,相关选项(-eva-context-depth
, -eva-context-width
, -eva-context-valid-pointers
).
因此,在您的情况下,设置 -eva-context-valid-pointers
将起作用。请注意,此选项会影响为初始状态创建的所有指针,因此如果有多个指针参数,则可能会出现问题。
另一种解决方案是编写一个前提条件,例如 /*@ requires\valid_read(foo); */
。 Eva 不会证明它(它将保持未知),但在分析过程中会考虑到它,从而防止发出警报。 Frama-C 的 future 版本可能包含一个admit
(或类似的关键字),以便能够声明此类属性并将其视为有效。
最后,对于更复杂的情况,可能需要更复杂的初始上下文,并且有插件可以做到这一点,但开源发行版中没有。在这种情况下通常做的是手动编写 stub 函数以在调用函数之前创建初始状态。一些 Frama-C 内置函数(例如 Frama_C_interval
)可用于帮助创建此状态。初始状态的一个例子是 available here,其中 argv
最多可以有 5 个任意字符串,每个字符串最多 256 个字符长。 .这种基于 stub 的方法提供了更高的精度,例如如果您有一个包含多个指针字段作为初始上下文的复杂结构,但它需要更多的努力。
关于c - 您如何告诉 Frama-C 和 Eva 入口点的参数被假定为有效?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/64242478/
当我使用 frama-c 分析我的 c 程序时。 frame-c 的影响插件中似乎存在一个错误。这是我的程序。 #include int global; int main() { global
抱歉,如果这在某处有详细说明,我尝试在 Frama-C 的不同文档中进行搜索,但没有走运。 我正在尝试在我的代码中进行死代码消除,但我不明白该工具的结果。是否有任何文件/文档可以解释此插件的工作原理?
我是 Frama-c 的新手,我想了解这个简单示例有什么问题: /*@ requires \valid(array+(0..length-1)) @ ensures \forall integer k
我有一个 16 位 MPU,它与 x86_16 的大小不同 size_t , ptrdiff_t等。谁能给我详细说明和明确说明如何在 Frama-C 中为我的 MPU 自定义机器依赖项? 最佳答案 目
我正在尝试使用 frama-c 验证以下代码段 /*@ ensures \result != \null; @ assigns \nothing; @*/ extern int *new_va
在 EVA tutorial ,我找到了这个截图:并解释:“导致此问题的确切值显示在列 c5 中:-1。C 标准将负数的左移视为未定义行为。因为 -1 是此调用堆栈中唯一可能的值,因此减少由警报引起的
我想分析一个大型项目的文件以使用 Frama-C 创建程序依赖图,但不断出现奇怪的错误,例如: /usr/include/bits/fcntl-linux.h:305:[kernel] user er
有人可以告诉我这是 Frama-C 中整数和无符号整数的非确定性值的正确模型吗? /* Suppose Frama-C is installed in /usr/local -default pref
使用某些基准运行 Frama-C 值分析时,例如susan 在 http://www.eecs.umich.edu/mibench/automotive.tar.gz 中,我们注意到很多 block
我想证明 Frama-C 中欧几里德除法的循环实现: /*@ requires a >= 0 && 0 =0; loop assigns q,r; loop variant r;
我正在尝试学习 ACSL,但在尝试编写完整的规范时遇到了困难。我的代码 #include #include #define NUM_ELEMS (8) /*@ requires expected
我尝试在 Windows 7 上运行 Frama-C,但没有成功。 我已阅读您在这里写的所有提示和评论,但仍然不起作用。 有人可以用一种清晰简单的方式解释安装过程吗,我将不胜感激? 最佳答案 Wind
我正在尝试在函数中插入断言。这是我所做的: void foo(int a) { //@ assert a == 1; } void main() { foo(1); foo(2);
我刚刚开始开发一个 frama-c 插件,该插件正在执行某种别名分析。我正在使用 Dataflow.Backwards 分析,现在我必须遍历不同的赋值语句并收集一些有关左值的内容。 frama-c 是
这感觉像是一个愚蠢的问题,但我被难住了。我正在尝试使用 Frama-C Sodium 和 Why3 0.86.1(均通过 OPAM 安装)来证明一些简单的属性。考虑这个程序 (toy.c): int
我正在尝试验证来自 Frama-C + WP 的简单程序。 #include /*@ requires valid_read_string(s); assigns \
尝试使用推荐的 opam 方法安装 Frama-C 会出现以下错误: ### stdout ### # Cleaning Installation directory # Installing
我找到的最接近的答案可能与 Eva 插件的 -absolute-valid-range 有关,但真的是这样吗?我是否必须想出读/写 ACSL 谓词来执行虚拟读/写? 示例代码: #include #
我想对多个 文件执行代码转换,并将这些转换产生的更改写回原文件,最好是原始文件。例如,我想向源自文件 fileA.c 的函数 funcA 和函数 funcB 添加一个 if 语句在文件 fileB.c
我应该如何证明如下代码的正确性,为了避免效率低下,它依赖于模运算? #include uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r
我是一名优秀的程序员,十分优秀!