alt-ergo не запускается на windows через cygwin

Question

Я пытаюсь запустить тестовый файл на frama-c с помощью средства проверки alt-ergo. Тем не менее, я получаю следующую ошибку с alt-ergo. Все остальные проверки Frama-C в порядке. Я знаю, что проблема не в тестовом файле.

------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
Fatal error: exception Sys_error("/tmp/wpf0dd65.dir/typed/test_post_2_Alt-Ergo.mlw: No such file or directory")
------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_test_post_2 : Failed
     Error: Alt-Ergo exits with status [2]

Я на машине с Windows и выполняю все установки через Cygwin в режиме администратора. Я получил Frama-C Neon и установил его с ./configure & make & make-installи установка прошла успешно (все проверки frama-c проходят в моем тестовом файле)

Я получил следующую версию двоичного файла alt-ergo Linux x86_64: alt-ergo-0.95.2-x86_64 с http://alt-ergo.ocamlpro.com/download.php. Я пошел с этой версией, так как документы frama-c запрашивают версию 0.95.

Я использовал следующие инструкции для установки alt-ergo ( https://www.lri.fr/~marche/MPRI-2-36-1/install.html)

Установка Альт-Эрго

Самый простой способ - получить бинарный файл alt-ergo. Загрузите файл "Linux x86_64 binary". Затем:

   chmod +x alt-ergo-0.95.2-x86_64 
   sudo cp alt-ergo-0.95.2-x86_64 /usr/bin/alt-ergo

при звонке which но frama-c и alt-ergo имеют правильный путь

$ which frama-c
/usr/bin/frama-c

$ which alt-ergo
/usr/bin/alt-ergo

У меня также есть Why3 установлен и он обнаруживает Ergo Prover

$ why3 config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
1 provers detected and 0 provers detected with unsupported version
Save config to /home/username/.why3.conf

---

редактировать

Я создал следующий test.mlw с онлайн-примером

type 'a set

logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop

axiom mem_add:
    forall x, y : 'a. forall s : 'a set.
    mem(x, add(y, s)) <->
    (x = y or mem(x, s))

logic is1, is2 : int set
logic iss : int set set

goal g:
    is1 = is2 -> 
    mem (is1, add (is2, iss))

запуск alt-ergo приводит к:

alt-ergo test.mlw
File "file.mlw", line 1, characters 1-26:Valid (0.0156) (0)

Есть идеи?

Answer 1

Следующее лечит симптомы: использование флага -wp-out с путем к Windows решит проблему

например

frama-c -wp -wp-print -wp-out c:/Users/userName/Desktop/tmp2 ../../cygdrive/c/Users/userName/Desktop/swap.c

Answer 2

Можете ли вы поместить следующий пример в "file.mlw"

goal hello_world: 1+1 = 2

а затем попробуйте выполнить ваши двоичные файлы Windows и / или Cygwin, указав в качестве входных данных файл "file.mlw"