frama-c - 一个可能无限的 C 函数的 ACSL 规范

Question

我试图指定外部函数的行为，更准确地说，它们的终止。ACSL 文档说该\terminates p;属性指定如果谓词p成立，则保证函数终止，但在p不成立时不指定任何内容。它还解释了一个永远不会返回的函数可以通过以下方式指定：

//@ ensures \false ; terminates \false ;

此外，ACSL 提供了一个属性\exits p;来指定在突然终止的情况下的后置条件。所以我想知道是否：

//@ ensures \false ; exits \false; terminates \false ;

会指定函数总是永远循环吗？

此外，规范是什么：

//@ ensures p ; exits q; terminates \false ;

意味着关于可能的无限循环？

Answer 1

您的规范是最接近可以说函数永远循环的规范，但我仍然看到两个极端情况：

1. 运行时错误：您总是可以说它们在其他地方得到处理（WP+genassigns或Value）
2. longjmp：恐怕目前 ACSL 中没有任何内容可以指定类似的内容。