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，声明的类型可以在vtype中的相应varinfo的字段中直接访问。对于指针，例如v，应该可以利用Value的结果来查看它们可能指向的位置，并使用它来派生适当的类型信息(主要问题是决定当值不精确时应该做什么，并给出几个具有不同类型的潜在位置)。