Início / coding / Perguntas / 77152086
Accepted
Carl
Asked: 2023-09-22 00:33:29 +0800 CST

Dafny: Como chamar 'verifcationLogger:csv'?

  • 772

Estou tentando depurar o tempo de verificação variável no Dafny. Tento executar o verifyLogger, mas não obtenho saída.

  • Estou no Windows (mas ficaria feliz com uma solução Linux)

  • Defino meu caminho para a versão do Dafny instalada pelo complemento VSCode, assim:

    definir caminho=C:\Usuários\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%caminho%

  • Eu corro:

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

mas não vejo nenhuma saída CSV.

dafny

2 respostas

  1. Best Answer

    Não estou familiarizado com o novo estilo de opções de linha de comando dafny, mas isso parece funcionar para mim (estou usando o estilo antigo de opção de linha de comando)

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

    Acho que o problema é que você está passando o verifyLogger após o boogie, o que significa que ele é enviado para o boogie, mas o verifyLogger é uma opção dafny

    • 1

  2. Descobri que isso funciona para dar detalhes do novo estilo:dafny verify --help

    Então eu posso fazer:

    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

    Alguém pode querer um número diferente de núcleos, um formato diferente (por exemplo, csv e sem "tee"), não usar Split, etc.

    (Mas agora que tenho os formatos *.txt e *.csv e *.trx, não sei o que fazer com eles. Vou começar uma nova pergunta.)

    • 0

relate perguntas