2

Windows環境でプラグインを介してcvc4証明者を使用しようとしています。システムにインストールしています。Why3 は、証明者として cvc4 を含めるように適切に構成されています。Frama-c wpWhy3frama-cwhy3

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

次のコマンドを使用して、frama-c Wp プラグインを使用して、.c ファイル (ACSL 仕様の C ソース ファイル) に対応する why3 形式 (.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使用して、生成されたファイルで Theories を証明しようとすると、次のエラーで失敗します。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 がインストールされていても、実行しても Prover はwhy3 config --detect追加されません。そのため、実行時に実行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) 証明者へのパスを適切に設定した後、次のように 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 ファイルを生成/tmpし、これらのファイルに対して証明者が呼び出されたときに、これらのファイルへの完全なパスが提供されておらず、証明者がそれについて不平を言うために発生しています。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"

Windowsパスからディレクトリ%fへのファイル形式を変更したことに注意してくださいC:/cygwin%f/tmp

于 2015-05-19T21:13:23.683 に答える