frama-c - 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 字节 block 都可以用于存储 32 位整数。

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