Frama-c 中的类型检查

Question

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

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

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

在精神上有什么类似的吗？

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

谢谢， 爱德华多

Answer 1

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

也就是说，Frama-C 是一个可扩展的平台，并且始终可以针对特定需求编写插件。对于示例中的x 等普通变量，声明的类型可以在AST 中相应varinfo 的vtype 字段中直接访问。对于指针，例如v，应该可以利用 Value 的结果来查看它们可能指向的位置并使用它来导出适当的类型信息（主要问题是决定当 Value 不精确时应该做什么并给出几个不同类型的潜在位置）。