- 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/
为了遵循务实的编程原则,我试图根据“告诉,不要询问”原则来决定如何处理用户密码更改。 我有一个用户对象,其密码每 30 天过期一次。如果密码过期,我需要能够显示密码过期/更改密码 View 。询问对象
我试图在接收文件时绕过任何本地存储。根据documentation ,如果“合理”,Flask 会将文件保存在内存中,否则会将它们存储在临时位置。 我只找到了一种通常使用 MAX_CONTENT_LE
SAS 在 proc 中返回 sci-notation 意味着总和输出,我不能将其用于进一步的速率计算过程。如何抑制 SAS 产生 sci-notation,有什么想法吗?提前致谢。 “解决了一个类似
当使用 nohup 时,脚本的输出会被缓冲,只有在脚本执行完毕后才会转储到日志文件 (nohup.out) 中。以接近实时的方式查看脚本输出以了解其进展情况将非常有用。有没有办法让 nohup 在脚本
假设我们定义了以下路由: const routes: Routes = [ { path: '', component: WelcomeComponent }, {
我正在尝试以下操作: a a > 1 1 > 2 2 > 3 3 我想要的是: a b > 1 1 > 2 2 > 3 3 有没有办法告诉 R 使用存储在对象( "b" )中的字符串( a
我想在安装二进制文件之前使用 automake 处理/修改它们。例如,我想将二进制文件中的符号提取到单独的文件和位置(如 this )。另一个示例是收集关键 Assets 的 md5sum 以发布报告
我的应用程序有一个主要的 pro 文件,我想告诉 qmake 在与应用程序同时编译一个单独的库。该库的目录中还有一个 pro 文件。这可能吗? 最佳答案 将 lib 和应用程序放在单独的子目录中,并使
我的 vimrc 中有以下内容: nnoremap :!screen -S foo -p run -X stuff '!!^M' 但是,当单击 F1 时,出现错误:没有上一个命令。 我想要的
我正在使用 Swagger 和 Scala 来记录我的 REST API。我想为 POST、PUT 和 DELETE 启用批量操作,并希望相同的路由接受单个对象或对象集合作为正文内容。 有没有办法告诉
我有一个 SAS 代码,它为我的计算创建了很多中间表。事情是,我在工作完成后并不真正关心这张 table ,我只关心决赛的结果。 但是,每次我运行这段代码时,SAS 都会添加所有生成的表来做我的流程,
有没有办法告诉 UglifyJS 跳过特定的代码部分,也许使用这样的注释: // uglifyjs:skipStart filter = function(item){ /* some crazy f
在 macOS 上通过 homebrew 安装包时,如果我的网络不稳定并且一次下载失败,homebrew 将下载源并从源开始构建。这将需要很长时间和高 CPU 使用率,这是不需要的。如何在下载失败时告
有没有办法告诉 GORM 不要保留属性?我计划在我的 User 类上定义一个确认密码属性,用于验证,但不应保留。 最佳答案 使用 transient 关键字 GORM 可以指示不持久化特定属性。 以下
我正在为 jQuery 编写一个幻灯片放映应用程序(单击按钮,然后滑动浏览图像列表),但我遇到了一个小错误,它将响应 即使在动画发生时也会发出 click() 请求。我已经在使用 animate()
我可以告诉 Xcode 4 我不在项目中使用自动布局吗? 目前,每个新创建的 xib 都会启用自动布局,这意味着我必须在创建 xib 后手动将其关闭,而我不希望这样。 最佳答案 这是自动布局的问题。您
因此,我正在使用目前手动运行的 AzCopy,但我要通过我们的一台服务器上的任务计划程序来运行它。如果我手动执行批处理文件,这会将文件从一个容器复制到另一个容器,并且可以完美运行。然而,它问我: Ov
我正在 OSX 中编写一个基于文档的应用程序。我发现当我更改文档的内容时,应用程序不知道文档已更改。我可以在没有警告的情况下关闭文档,这会导致我未保存的内容丢失。 如何告诉 NSDocument 文档
根据NSWindow Class Reference ,您应该“很少需要调用”NSWindow 方法“display”或“setViewsNeedDisplay”。那么重新显示窗口内容的常用方法是什么
为了重写开源 iMedia 框架项目(目前有数十名开发人员正在使用),我们正在切换到 IKImageBrowserView,并且在缓存方面遇到了麻烦。 看来 IKImageBrowserView 喜欢
我是一名优秀的程序员,十分优秀!