Why3无法通过cygwin在windows上运行验证程序。

Question

在Windows环境下，我试图通过cvc4通过Why3使用Frama-c wp插件的Why3验证器。我的系统上安装了frama-c和why3。Why3被正确地配置为包括cvc4作为验证程序：

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

我使用frama-c Wp插件生成与我的why3文件(C源文件具有ACSL规范)对应的.why格式(.why)文件，并使用以下命令：

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

上面的命令在swap_Why3_ide.why目录中生成一个文件C:/Users/user/temp/typed。

当我试图用以swap_Why3_ide.why为证明器的why3来证明生成的cvc4文件中的理论时，它失败了，但有以下错误：

$ 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.

我在linux环境中执行了相同的步骤，why3能够执行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) 

有人能建议如何在windows上执行Why3吗？

Answer 1

似乎没有人在Windows上使用why3。但是无论如何，对于将来尝试在windows上使用Why3的人来说，下面是我在.why文件中运行一个理论证明的步骤：

1)在Windows上，即使安装了验证程序，执行why3 config --detect也不会添加验证程序。因此，在执行why3 config --detect --add-prover cvc4 path_to_executable_in_Windows_format时，确保可执行文件的路径为windows格式(例如C：\provers\cvc4-1.4Win32-opt.exe)

如果路径不采用windows格式，则引发下列错误：

/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)正确设置验证程序的路径后，尝试按以下方式执行why3：

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

这将引发以下错误：

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

发生此错误是因为why3在cygwin目录(/tmp)中生成*.smt2文件，并且当在这些文件上调用验证程序时，未提供这些文件的完整路径，并且验证程序抱怨它是Couldn't open file /tmp/XX.smt2的。

要解决这个问题，我必须执行update命令才能在.why3.conf中运行prover，如下所示：

[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"

请注意，我将文件格式从%f更改为C:/cygwin%f，这是指向/tmp目录的windows路径。