可能無限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指定類似的東西。