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

Question

Я пытаюсь запустить тестовый файл на frama-c с помощью альт-эрго-теста. Тем не менее, я получаю ошибку followng с 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] 

Я на окна машины и выполнять все установки с помощью Cygwin в режиме администратора я получил Frama-C Неон и установил его с ./configure & make & make-install, и установка прошла успешно (все Фрама-с проверки проходят в моем тестовом файле)

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

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

Установка Alt-эргономичной

Самый простой способ, чтобы получить двоичный файл альт-эргометра. Скачать файл под названием «Linux x86_64 двоичным» Тогда:

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

при вызове which но Frama-с и альт-эрго есть правильный путь

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

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

Я также why3 установлен и он обнаруживает Ergo испытатель

$ 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 test.mlw 
File "file.mlw", line 1, characters 1-26:Valid (0.0156) (0) 

Любые идеи?

Answer 1

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

, например

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» в качестве входных данных