c - frama-c 切片插件似乎丢弃了使用的堆栈值
问题描述
问题描述
我正在开发一个 frama-c 插件,它使用切片插件作为库来删除自动生成的代码中未使用的位。不幸的是,切片插件丢弃了一堆实际使用的堆栈值。只要它们的地址包含在传递给抽象外部功能的结构中,就可以使用它们。
简单的例子
这是一个更简单的示例,它模拟了我拥有的相同的一般结构。
/* Abstract external function */
void some_function(int* ints[]);
int main() {
int i;
int *p = &i;
int *a[] = { &p };
some_function(a);
return 0;
}
frama-c-gui -slice-calls some_function experiment_slicing.c
当使用(我还没有弄清楚在没有 gui 的情况下调用命令行时如何查看切片输出)对这个示例进行切片时,它会删除除声明int *a[];
和对some_function
.
尝试修复
我尝试通过添加 ACSL 注释来修复它。但是,我认为合理的规范(见下文)不起作用
/*@ requires \valid(ints) && \valid(ints[0]);
*/
void some_function(int* ints[]);
然后我尝试了一个具有所需行为的分配(见下文)。然而,这不是一个正确的规范,因为该函数实际上从未写入指针,而是需要读取它以获得正确的功能。我担心如果我继续使用这种不正确的规范,它会导致奇怪的问题。
/*@ requires \valid(ints) && \valid(ints[0]);
assigns *ints;
*/
void some_function(int* ints[]);
解决方案
您在正确的轨道上:这是assigns
您应该在这里使用的子句:它将指示内存状态的哪些部分与对未定义函数的调用有关。但是,您需要提供一个完整的assigns
子句及其\from
部分(指示读取哪个内存位置以计算写入的内存位置的新值)。
我int
在您的示例中添加了一个变量,因为您的函数没有返回结果(void
返回类型)。对于返回某些内容的函数,您还应该有一个子句assigns \result \from ...;
:
int x;
/*@ assigns x \from indirect:ints[..], *(ints[..]); */
void some_function(int* ints[]);
int main() {
int i;
int*p = &i;
int *a[] = { &p };
some_function(a);
return 0;
}
该assigns
子句表示some_function
可能会更改 的值x
,并且新值将根据存储在其中的地址计算ints[..]
(indirect
标签告诉我们不直接使用它们的值,这在Eva 手册的第 8.2 节中有更详细的描述) ,以及它们的内容。
using frama-c -slice-calls some_function file.c -then-last -print
(最后一个参数在这里用于在标准输出上打印结果文件:-then-last
表示以下选项应该对创建的最后一个 Frama-C 项目进行操作,在这种情况下是切片产生的项目,并-print
打印所述的 C 代码项目。您也可以使用-ocode output.c
将代码的漂亮打印重定向到output.c
.) 给出以下结果:
* Generated by Frama-C */
void some_function(int **ints);
void main(void)
{
int i;
int *p = & i;
int *a[1] = {(int *)(& p)};
some_function(a);
return;
}
另外请注意,您的示例类型不正确:&p
是指向 int 的指针,因此应存储在int**
数组中,而不是int*
数组中。但我认为它只是源于减少你原来的例子,对于切片本身并不重要。
推荐阅读
- jquery - data-confirm-modal:似乎没有加载引导模式插件
- bash - Kafka MongoDB 接收器连接器错误!没有开始
- swift - SwiftUI 自定义视图永远重复动画显示为意外
- rust - 使用 extern 命令时找不到 crate
- firebase - 无法为 firebase 中的 bigquery 链接启用 google 分析
- android - 使用 FCM 发送通知时如何使用图像 URL?
- c# - 网站安全 - 1 个主站点,1 个在主站点内托管的辅助站点
- javascript - 在这段代码中,resolve 和 reject 做什么?
- android - Unity ARFoundation App Crash - 空指针取消引用问题
- axon - Axon 自动创建的表格有什么用?