如何调用Dafny的verificationLogger:csv？运行无CSV输出求助

核心修复与排查点 #

• 修正Boogie参数传递格式：你命令里重复用了--boogie，导致-verificationLogger:csv没正确传给Boogie。正确的做法是把所有Boogie参数打包在同一个--boogie后面，用引号包裹：

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

  或者用--boogie-opt逐个传递参数，避免格式错误：

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

  重复调用--boogie会让Dafny把后续参数当成自己的命令解析，根本传不到Boogie那边，这大概率是你没拿到输出的原因。

• 确认文件有可验证内容：如果repro1.dfy里没有断言、不变式或者方法合约这类需要验证的代码，Boogie不会执行验证流程，自然不会生成日志。先给文件加个简单的可验证片段测试：

  method Test() {
    var x := 5;
    assert x > 0;
  }
  

• 检查输出路径与权限：CSV日志默认生成在当前工作目录，文件名是verification-log.csv。确认你有当前目录的写入权限，也可以手动指定输出路径避免歧义：

  --boogie "-verificationLogger:csv:my-verify-log.csv"
  

• 验证版本兼容性：你用的是Dafny 4.2.0，先确认对应版本的Boogie支持-verificationLogger参数。直接在你的Dafny安装路径下运行boogie /help，看看参数列表里有没有这个选项，部分旧版本可能不支持或者参数名有变化。

额外调试步骤 #

• 单独测试Boogie：先把Dafny文件编译成Boogie格式，再直接用Boogie运行，排查是Dafny传参问题还是Boogie本身的问题：

  dafny compile --target:boogie repro1.dfy
  boogie -verificationLogger:csv repro1.bpl
  

  如果这步能生成CSV，说明问题出在Dafny的参数传递环节；还是不行的话，要么是文件没验证内容，要么是Boogie版本不兼容。

• 查看参数传递详情：给Dafny命令加--trace参数，能看到参数传递的完整过程，确认-verificationLogger是否真的传给了Boogie：

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

内容的提问来源于stack exchange，提问作者Carl