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 中没有任何内容可以指定类似的内容。