2

我正在尝试在 Windows 环境中使用cvc4带有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 插件使用以下命令生成与我的 .c 文件（具有 ACSL 规范的 C 源文件）相对应的为什么 3 格式（.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目录 中生成一个文件。

当我尝试使用with作为证明者来证明生成swap_Why3_ide.why文件中的理论时，它失败并出现以下错误：why3cvc4

$ 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能够执行证明程序：

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？

4

1 回答 1

2

似乎没有人在 Windows 上使用Why3。但无论如何，对于将来尝试在 Windows 上使用 Why3 的​​任何人，以下是我执行的步骤，用于在 .why 文件中运行理论证明器：

1）在Windows上，即使安装了prover，执行why3 config --detect也不会添加prover。因此，在执行时why3 config --detect --add-prover cvc4 path_to_executable_in_Windows_format请确保可执行文件的路径为 Windows 格式（例如 C:\provers\cvc4-1.4-win32-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）正确设置provers的路径后，尝试执行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 目录 ( /tmp) 中生成 *.smt2 文件，并且当通过这些文件调用证明者时，未提供这些文件的完整路径并且证明者抱怨它Couldn't open file /tmp/XX.smt2

为了解决这个问题，我必须更新执行以运行证明者的命令.why3.conf，如下所示：

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

请注意，我将文件格式从%fWindowsC:/cygwin%f路径更改为/tmp目录

于 2015-05-19T21:13:23.683 回答