Спецификация ACSL для возможно бесконечной функции C

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 указать что-то подобное.