3

I am trying to run a test file on frama-c with the alt-ergo prover. However,I am getting the followng error with alt-ergo. All the other frama-c checks are fine. I know that the issue 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 perform all of the installations via cygwin in administrator mode I got frama-C Neon and installed it with ./configure & make & make-install, and the installation was successful ( all the frama-c checks pass in my test file)

I got the following version of alt-ergo Linux x86_64 binary: alt-ergo-0.95.2-x86_64 from http://alt-ergo.ocamlpro.com/download.php. I went with this version, since the frama-c docs ask for version 0.95.

I used the following instructions to install alt-ergo (https://www.lri.fr/~marche/MPRI-2-36-1/install.html)

Installation of Alt-ergo

The simplest way is to get the binary file of alt-ergo. Download the 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 calling which but frama-c and alt-ergo have a correct path

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

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

I also have why3 installed and it detects the 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 the 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))

running alt-ergo results in:

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

Any ideas?

Quantico
  • 2,398
  • 7
  • 35
  • 59
  • Hi. Have you tried to execute directly Alt-Ergo on /tmp/wpf0dd65.dir/typed/test_post_2_Alt-Ergo.mlw ? Or to install it from sources ? – iguerNL Sep 17 '14 at 19:50
  • @MohamedIguernlala I am not sure how to do that. Also /tmp/wpf... is a temporary directory that is not being created. I think the issue is that it is a windows machine, but the installation was made via cygwin (as why3,alt-ergo,frama-c required) so it has an issue with finding this path. – Quantico Sep 17 '14 at 19:52
  • I downloaded alt-ergo for windows (just the .exe file) and put it in the path. trying to run ./alt-ergo.exe results in my terminal just hanging there. as for /tmp/..../ no such directory exist. Every run generates a different tmp/random_name_directory. I think the issue is windows/cygwin related. Any ideas? – Quantico Sep 18 '14 at 03:43
  • If you execute Alt-Ergo without input file, it'll read data from standard input. – iguerNL Sep 18 '14 at 04:28

2 Answers2

4

The following treats the symptoms: using the -wp-out flag with a windows path will solve the issue

for example 

frama-c -wp -wp-print -wp-out c:/Users/userName/Desktop/tmp2 ../../cygdrive/c/Users/userName/Desktop/swap.c
Quantico
  • 2,398
  • 7
  • 35
  • 59
1

Can you put the following example in a "file.mlw"

goal hello_world: 1+1 = 2

and then, try to execute your Windows and/or Cygwin binaries by providing "file.mlw" as input

iguerNL
  • 464
  • 2
  • 8