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

Question

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

/*@
    ensures \result >= x && \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.

Answer 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.