Ошибка пользователя: проверка 'alt-ergo' не найдена в why3.conf

#frama-c #why3 #alt-ergo

#frama-c #почему 3 #alt-ergo

Вопрос:

Я пытаюсь протестировать функцию с помощью Frama-c:

 /*@
    ensures result >= x amp;amp; result >= y;
    ensures result == x || result == y;
*/

int max( int x, int y){
    return (x>y) ? x : y;
}

После того, как я установил все требования: OPAM, why3, alt-ergo
Всякий раз, когда я выполняю frama-c -wp fct.c, я получаю:

 [kernel] Parsing fct.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] Goal typed_max_ensures : not tried
[wp] Goal typed_max_ensures_2 : not tried
[wp] User Error: Deferred error message was emitted during execution. 
See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.

Ответ №1:

Как указано в инструкции по установке Frama-C, why3 он должен быть явно настроен для проверки доступных проверяющих с помощью why3 config --detect команды (обратите внимание, что в зависимости от точной версии Why3, которую вы установили, вы также можете использовать why3 config --full-config вместо этого). Вы должны увидеть вывод, подобный:

 Found prover Alt-Ergo version 2.0.0, OK.
... possibly other provers if you have installed them
Save config to /PATH/TO/HOME/.why3.conf

После этого вы сможете использовать проверки в Frama-C / WP

1. Я попробовал две команды, но это то, что я получаю: Found prover Coq version 8.12.0, but no Why3 libraries were compiled for it Prover Alt-Ergo version 2.3.3 is not known to be supported. Known versions for this prover: 2.3.1, 2.3.0. Known old versions for this prover: . 1 prover(s) added (including 1 prover(s) with an unrecognized version) Generating strategies: Save config to /Users/aliissaoui/.why3.conf

2. Если вы не планируете использовать coq для завершения проверки Frama-C или Why3, первый пункт не должен быть проблемой (но вы можете установить пакет opam why3-coq ). Второй момент — это просто указание на то, что ваша версия Why3 не была протестирована повторно с вашей версией Alt-Ergo. Учитывая близость с полностью поддерживаемыми версиями (2.3.3. vs. 2.3.1), это не должно быть проблемой, но если при выполнении проверки возникают сбои Alt-Ergo, вы можете рассмотреть возможность понижения версии до 2.3.1.

3. Похоже, что командная строка изменилась? Мне нужно why3 config detect , у меня есть why3 v1.4.0. Похоже opam install why3 , что пытается вам это сказать. Последнее сообщение => Why3 проверяет настройку: rm -f ~/.why3.conf ; обнаружение конфигурации why3 , но если вы никогда не использовали opam, неясно, что это инструкции для пользователя. Я думал, что это команда, которая была выполнена opam.

4. @artlessnoise да, why3 менял синтаксис командной строки для обнаружения проверяющих три раза за последние три выпуска (но разработчик, говорящий на условиях строгой анонимности 😛, пообещал мне, что 1.4.0 был последним разом). Обычно каждая инструкция по установке Frama-C содержит соответствующую командную строку для соответствующей версии Why3.