Alt-ergo won't start on windows via cygwin
I am trying to run a test file in frama-c using alt-ergo. However, I am getting followng error with alt-ergo. All other frama-c checks are fine. I know the problem is not with the test file.
------------------------------------------------------------
--- 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]
I am on a windows machine and doing all installations through cygwin in admin mode I got frama-C Neon and installed it with ./configure & make & make-install
and the installation was successful (all frama-c checks pass in my test file)
I got the following version of the Linux x86_64 alt-ergo binary: alt-ergo-0.95.2-x86_64 from http://alt-ergo.ocamlpro.com/download.php . I went with this version as the frama-c docs request version 0.95.
I used the following instructions to install alt-ergo ( https://www.lri.fr/~marche/MPRI-2-36-1/install.html )
Installing Alt-ergo
The easiest way is to get the alt-ergo binary. Download a file called "Linux x86_64 binary" Then:
chmod +x alt-ergo-0.95.2-x86_64
sudo cp alt-ergo-0.95.2-x86_64 /usr/bin/alt-ergo
when called which
, but frama-c and alt-ergo have the correct path
$ which frama-c
/usr/bin/frama-c
$ which alt-ergo
/usr/bin/alt-ergo
I also have why3 and it detects 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
Edit
I created the following test.mlw with an online example
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))
Executing alt-ergo results in:
alt-ergo test.mlw
File "file.mlw", line 1, characters 1-26:Valid (0.0156) (0)
Any ideas?
source to share