2

我想知道 Frama-C 是否实现了某种与指针相关的类型检查。例如，考虑以下情况：

int x[10];
void * v = x;

//@ assert isOfTypeInt(x, 10)
//@ assert isOfTypeInt(v, 10)

有没有和上面类似的精神？

看 ACSL 手册，有很多方法可以检查内存和指针的使用情况（其中一部分是在 Frama-C Oxygen 中实现的）。不过，我还没有找到任何通用的支持来处理类型信息。是否有我们可以用于此目的的 frama-c 插件？

谢谢，爱德华多

4

1 回答 1

2

ACSL 中确实没有这样的东西。事实上，C 中的内存位置并没有真正与它们相关的类型信息：如果我们忽略潜在的对齐约束，任何 4 字节的块都可以用于存储 32 位整数。

也就是说，Frama-C 是一个可扩展的平台，并且总是可以为特定需求编写插件。对于您的示例中的普通变量，声明的类型可以在AST中对应的字段中x直接访问。对于指针，如不同种类）。vtypevarinfov

于 2012-11-15T08:42:51.613 回答