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?
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