probar

Prueba un paquete de mudanza

Esta es una herramienta para la verificación formal de un paquete Move utilizando el probador Move.

Uso

movement aptos move prove [OPTIONS]

Opciones

• --dev Habilita el modo de desarrollo, que utiliza todas las direcciones y dependencias de desarrollo. El modo de desarrollo permite cambiar dependencias y direcciones a los campos preestablecidos [direcciones de desarrollo] y [dependencias de desarrollo]. Esto funciona tanto dentro como fuera de las pruebas para usar valores preestablecidos. Actualmente, también incorpora todos los artefactos de compilación de prueba.

• --package-dir <PACKAGE_DIR> Ruta a un paquete de movimiento (la carpeta con un archivo Move.toml).

• --output-dir <OUTPUT_DIR> Ruta para guardar el paquete de movimiento compilado. El valor predeterminado es <package_dir>/build.

• --named-addresses <NAMED_ADDRESSES> Direcciones con nombre para el binario de movimiento. Ejemplo: alicia=0x1234, bob=0x5678. Nota: Esto fallará si hay duplicados en el archivo Move.toml, elimínelos primero. [por defecto: ]

• --skip-fetch-latest-git-deps Evite extraer las últimas dependencias de git. Esto permitirá anular esto para el desarrollo local.

• --bytecode-version <BYTECODE_VERSION> Especifique la versión del código de bytes que emitirá el compilador.

• -v, --verbosity <VERBOSITY> Nivel de verbosidad.

• -f, --filter <FILTER> Filtra objetivos del paquete. Cualquier módulo con un nombre de archivo coincidente será un objetivo, similar a cargo test.

• -t, --trace Si se debe mostrar información adicional en los informes de errores. Esto puede ayudar a la depuración pero también puede hacer que la verificación sea más lenta.

• --cvc5 Si se debe utilizar cvc5 como backend del solucionador smt. La variable de entorno CVC5_EXEdebe apuntar al binario.

• --stratification-depth <STRATIFICATION_DEPTH> La profundidad hasta la cual se expanden las funciones estratificadas. [predeterminado: 6]

• --random-seed <RANDOM_SEED> Una semilla para el probador. [predeterminado: 0]

• --proc-cores <PROC_CORES> El número de núcleos que se utilizarán para el procesamiento paralelo de las condiciones de verificación. [predeterminado: 4]

• --vc-timeout <VC_TIMEOUT> Un tiempo de espera (suave) para el solucionador, por condición de verificación, en segundos. [predeterminado: 40]

• --check-inconsistency Si se debe verificar la coherencia de las especificaciones mediante la inyección de afirmaciones imposibles.

• --keep-loops Si se deben mantener los bucles como están y pasarlos al solucionador subyacente.

• --loop-unroll <LOOP_UNROLL> Número de iteraciones para desenrollar bucles.

• --stable-test-output Si la salida para, por ejemplo, el diagnóstico debe ser estable/redactada para que pueda usarse en la salida de prueba.

• --dump Ya sea para volcar los resultados del paso intermedio en archivos.