1

我已经从源代码编译并安装了两个 cvc4。按照建议下载并安装了 Cvc4，并从其 git 存储库下载了 Cryptol。沙盒和安装完成且没有错误（使用 GHC 7.8.3 x86_64）。该问题仅在调用cryptol并发出:prove True. 这是一切：

athan@namek ~/lib> cryptol
                        _        _
   ___ _ __ _   _ _ __ | |_ ___ | |
  / __| '__| | | | '_ \| __/ _ \| |
 | (__| |  | |_| | |_) | || (_) | |
  \___|_|   \__, | .__/ \__\___/|_|
            |___/|_| version 2.1.0 (8898348)

Loading module Cryptol
Cryptol> :prove True
cryptol: fd:6: hGetLine: end of file
athan@namek ~/lib>

对此的任何帮助都将是巨大的。对我来说，感觉就像找不到共享库。这会导致这个问题吗？谢谢你。

4

1 回答 1

1

总结评论中的对话：

问题中提到的“文件结尾”错误通常归因于感兴趣的证明者（在这种情况下为 CVC4）只是“部分安装”-在我的情况下，这始终是共享库的问题，可以通过调用命令行中的二进制文件（cvc、boolector 等）。REPL 将终止的错误的票在 Cryptol 的 github 上。幸运的是，该问题已在上游 SBV 中修复，并将很快出现在 Cryptol 的 SBV 分叉中。

WRT AthanClark 的特殊情况仍然未知为什么 CVC4 在被 Cryptol 调用时失败以及如何失败 - 可能性包括 cryptol 调用与我们期望的二进制文件不同的二进制文件或环境差异，例如 LD_LIBARARY 路径变量。无论哪种方式，听起来他都能够boolector成功地使用替代证明者 ( )。

编辑：如果您可以产生 Athan 的错误，其中 CVC 在 SBV 之外而不是 SBV 内部工作......并且您住在波特兰然后给我发消息，出现在我的办公室并给我看，我会感兴趣的。

于 2014-11-23T21:48:02.537 回答