一个可能无限的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

你的规范是最接近的，可以说一个函数是永远循环的，但我仍然看到了两个角落的情况：

ACSL运行时错误:您总是可以说它们在其他地方得到了处理(+

1. 或Value)
2. longjmp：，我担心在genassigns中目前还没有指定这样的东西。