主页 / coding / 问题 / 77152086
Accepted
Carl
Asked: 2023-09-22 00:33:29 +0800 CST

Dafny：如何调用“verifcationLogger:csv”？

  • 772

我正在尝试在 Dafny 中调试变量验证时间。我尝试运行verificationLogger，但没有得到任何输出。

  • 我使用的是 Windows（但对 Linux 解决方案很满意）

  • 我将路径设置为 VSCode 加载项安装的 Dafny 版本，如下所示：

    设置路径=C:\Users\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%

  • 我跑：

    dafny verify --verification-time-limit:15 --cores:6 --boogie -randomSeedIterations:10 --boogie -verificationLogger:csv repro1.dfy

但我没有看到 CSV 输出。

dafny

2 个回答

  1. Best Answer

    我不熟悉新风格的 dafny 命令行选项，但这似乎对我有用（我正在使用旧风格的命令行选项）

    dafny  /compile:0 /verificationLogger:csv repo1.dfy

    我认为问题是你在 boogie 之后传递 verifyLogger 这意味着它被发送到 boogie 但 verifyLogger 是 dafny 选项

    • 1

  2. 我发现这可以提供新样式的详细信息：dafny verify --help

    然后我可以这样做：

    dafny verify seq_of_sets_example7.dfy --verification-time-limit:45 --cores:20 --log-format text --boogie -randomSeedIterations:10 --boogie -vcsSplitOnEveryAssert | tee TestResults\del3.txt

    其他人可能想要不同的核心数、不同的格式（例如 csv 并且没有“tee”）、不使用 Split 等。

    （但现在我有 *.txt 和 *.csv 和 *.trx 格式，我不知道如何处理它们。我将开始一个新问题。）

    • 0

相关问题