2

I am trying to use cvc4 prover with Frama-c wp plugin through Why3 on Windows environment. I have frama-c and why3 installed on my system. Why3 is configured properly to include cvc4 as a prover :

$ why3 --list-provers
Known provers:
Alt-Ergo (0.95.2)
CVC4 (1.4)

I used frama-c Wp plugin to generate why3 format (.why) file corresponding to my .c file (C source file with ACSL Specifications) with following command:

frama-c -wp -wp-print -wp-proof-trace -wp-out C:/Users/user/temp -wp-prover cvc4 swap.c

The above command generate a file swap_Why3_ide.why in C:/Users/user/temp/typed directory.

When I try to prove Theories in generated swap_Why3_ide.why file using why3 with cvc4 as prover it fails with following error:

$ why3 prove -P cvc4 -L C:/cygwin/usr/local/share/frama-c/wp/why3 temp/typed/swap_Why3_ide.why

temp/typed/swap_Why3_ide.why VCswap_post WP : HighFailure (0.02s)
Prover exit status: exited with status 1

Prover output:
/usr/local/lib/why3/why3-cpulimit: Error: failed when launching <"/cygdrive/c/cvc4-1.4-win32-opt.exe" "--lang=smt2" "/tmp/why_29ba75_swap_Why3_ide-T-WP.smt2">
Fatal: CreateProcess failed with error 0: The operation completed successfully.

I performed same steps on a linux environment and why3 was able to execute prover:

why3 prove -P cvc4 -L /usr/local/share/frama-c/wp/why3/ temp/typed/swap_Why3_ide.why
temp/typed/swap_Why3_ide.why VCswap_post WP : Valid (0.05s)

Can anyone suggest how to execute Why3 on windows?

Gunjan Aggarwal
  • 710
  • 5
  • 19

1 Answers1

2

It seems like no one is using why3 on Windows. But anyways, for anyone who will try to use Why3 on windows in future, here are steps I performed to run a prover on theories in a .why file:

1) On Windows, even if provers are installed, executing why3 config --detect will not add provers. So when executing why3 config --detect --add-prover cvc4 path_to_executable_in_Windows_format make sure that path to executable is in windows format( for example C:\provers\cvc4-1.4-win32-opt.exe)

If path is not in windows format, following error is thrown:

/usr/local/lib/why3/why3-cpulimit: Error: failed when launching <"/cygdrive/c/cvc4-1.4-win32-opt.exe" "--lang=smt2" "/tmp/why_29ba75_swap_Why3_ide-T-WP.smt2">
Fatal: CreateProcess failed with error 0: The operation completed successfully.

2) After setting path to provers properly, try to execute why3 as follows:

why3 prove -P cvc4 -L C:/cygwin/usr/local/share/frama-c/wp/why3 C:/temp/typed/swap_Why3_ide.why

This will throw following error:

C:/temp/typed/swap_Why3_ide.why VCswap_post WP : HighFailure (0.03s)
Prover exit status: exited with status 1
Prover output:
(error "Couldn't open file: /tmp/why_727ef8_swap_Why3_ide-T-WP.smt2")
why3cpulimit cpu time: 0.015625s wall time: 0.015625s

This error is occurring because why3 generates *.smt2 files in cygwin tmp directory (/tmp) and when provers are called over these files complete path to these files in not provided and prover complain that it Couldn't open file /tmp/XX.smt2

To fix this I had to update command executed to run prover in .why3.conf as following:

[prover]
command = "%l/why3-cpulimit %t %m -s C:/provers/cvc4-1.4-win32-opt.exe --lang=smt2 C:/cygwin%f
driver = "/usr/local/share/why3/drivers/cvc4.drv"
editor = ""
in_place = false
interactive = false
name = "CVC4"
shortcut = "cvc4"
version = "1.4"

Note that I changed the file format from %f to C:/cygwin%f which is windows path to /tmp directory

Gunjan Aggarwal
  • 710
  • 5
  • 19