cpachecker

Comenzando con Cpachecker

• Instrucciones de instalación
• Pautas de contribución
• Instrucciones de desarrollo

Se puede encontrar más documentación en el doc/ Directorio.

Licencia y derechos de autor

Cpachecker tiene licencia bajo la licencia Apache 2.0 con derechos de autor de Dirk Beyer y otros (cf. Autors.md para la lista completa de todos los contribuyentes). Las bibliotecas de terceros están bajo otras licencias y derechos de autor, cf. Los archivos en las LICENSES directorio para los textos completos de la licencia. En particular, MathSAT está disponible solo para fines de investigación y evaluación (cf. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ), así que asegúrese de usar un solucionador SMT diferente si es necesario. Tenga en cuenta que aunque un programa GPL se distribuye junto con Cpachecker, Cpachecker está separado de ese programa y, por lo tanto, no bajo los términos de la GPL.

Prepare programas para la verificación de Cpachecker

Todos los programas deben preprocesar con el preprocesador C, es decir, es posible que no contengan las directivas #define y #include . Puede habilitar el preprocesamiento dentro de Cpachecker especificando --preprocess en la línea de comandos. Se pueden administrar varios archivos C y se vincularán y se verificarán como un solo programa (característica experimental).

Cpachecker puede analizar y analizar un gran subconjunto de (GNU) c. Si el análisis falla para su programa, envíe un informe a [email protected].

Verificación de un programa con cpachecker

1. Elija un archivo de código fuente que desee ser verificado. Si usa su propio programa, recuerde preprocesarlo como se mencionó anteriormente. Ejemplo: doc/examples/example.c o doc/examples/example_bug.c Una buena fuente para programas más de ejemplo es el repositorio de Benchmars SV que, por ejemplo, es utilizado por la competencia internacional sobre la verificación del software.

2. Opcionalmente: si desea elegir ciertos análisis como el análisis de predicado, especifique un archivo de configuración. Este archivo define, por ejemplo, qué CPA se utilizan. Los archivos de configuración estándar se pueden encontrar en el directorio config/ . Si no desea un análisis específico, recomendamos la configuración predeterminada de Cpachecker. Sin embargo, tenga en cuenta que si está en MACOS, debe proporcionar binarios de MathSAT compilados específicamente para que funcione la configuración predeterminada (o use Docker para ejecutar la versión Linux de Cpachecker). La configuración de CPACHECKER se explica en doc/Configuration.md .

3. Elija un archivo de especificación (es posible que no necesite esto para algunas configuraciones). Las configuraciones estándar utilizan config/specification/default.spc como la especificación predeterminada. Con este, CPACHECKER buscará etiquetas llamadas ERROR (insensible al caso) y las afirmaciones en el archivo del código fuente. Se pueden encontrar otros ejemplos de especificaciones en config/specification/ en el directorio CPACHECKER.

4. Ejecutar bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> Los argumentos de línea de comandos adicionales se describen en doc/Configuration.md . Para usar la configuración predeterminada de Cpachecker, pase solo el archivo fuente: bin/cpachecker doc/examples/example.c . Se puede elegir un análisis específico (como la inducción K), por ejemplo, con bin/cpachecker --config/kInduction.properties doc/examples/example.c o la abreviatura equivalente bin/cpachecker --kInduction doc/examples/example.c . Java 17 o posterior es necesario. Si no está en su camino, debe especificarlo en la variable de entorno Java. Ejemplo: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java para 64 bits openjdk 17 en ubuntu.

   Tenga en cuenta que no todas las configuraciones de análisis están disponibles para macOS porque no enviamos binarios para solucionadores SMT para esta plataforma. Usted necesita construir los binarios apropiados usted mismo o usar análisis menos potentes que funcionen con solucionadores basados ​​en Java, por ejemplo, este en lugar de la configuración predeterminada de Cpachecker: --predicateAnalysis-linear --option solver.solver=SMTInterpol Of R, de curso, también puede usar soluciones como Docker para ejecutar la versión de Linux de Cpachecker.

   Si instaló cpachecker usando Docker, la línea de comando de ejemplo anterior se vería así: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c Este comando hace que el directorio actual esté disponible en el contenedor, por lo que a verificar un programa en el directorio actual solo proporciona su nombre de archivo en lugar de el ejemplo en lugar del ejemplo, es el ejemplo que está disponible con el ejemplo que es el ejemplo que está disponible con el ejemplo que es el ejemplo que es el ejemplo que es el ejemplo que es el ejemplo que es el ejemplo que está disponible en el ejemplo de su ejemplo. Cpachecker. Los archivos de salida de Cpachecker se colocarán en ./output/ .

5. Además de la salida de la consola, se genera un informe HTML interactivo en la output/ , ya sea nombrado Report.html (para el resultado verdadero) o Counterexample.*.html (para el resultado falso). Abra estos archivos en un navegador para ver el resultado del análisis CPACHECKER (cf. doc/Report.md )

También hay archivos de salida adicionales en la output/ :

• ARG.dot : Visualización del árbol de acachabilidad abstracto (formato GraphViz)
• cfa*.dot : Visualización del flujo de control Automaton (formato GraphViz)
• reached.dot .
• coverage.info : Información de cobertura (similar a las de las herramientas de prueba) en formato Gcov Use la siguiente línea de comando para generar un informe HTML como output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : una ruta a través del programa que conduce a un error
• Counterexample.*.assignment.txt : Asignaciones para todas las variables en la ruta de error.
• Counterexample.*.harness.c : un arnés de prueba que puede reproducir la ruta de error a través de la ejecución de la prueba. Consulte DOC/Tutorials/Test-Harness.md para un uso de ejemplo.
• predmap.txt : predicados utilizados por análisis de predicado para probar la seguridad del programa
• reached.txt : volcado de todos los estados abstractos alcanzados
• Statistics.txt : estadísticas de tiempo (también se pueden imprimir para consolar con --stats )

Tenga en cuenta que no todos estos archivos estarán disponibles para todas las configuraciones. Además, algunos de estos archivos solo se producen si se encuentra un error (o viceversa). ¡Cpachecker sobrescribirá archivos en este directorio!

Validación de un programa con CPA-Witness2Test

Puede validar testigos de violación con CPA-Witness2Test, que forma parte de Cpachecker.

1. Para hacerlo, necesita un testigo de violación, un archivo de especificación que se ajuste al testigo de violación y el archivo del código fuente que se ajuste al testigo de violación.

2. Para validar al testigo, ejecute el siguiente comando:

    bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
   

   Los argumentos de línea de comandos adicionales se ven con bin/cpa-witness2test -h .

3. Cuando termine, y si el testigo de violación se valida con éxito, la salida de la consola muestra Verification result: FALSE . Además de la salida de la consola, CPA-Witness2Test también crea una output/*.harness.c . Este archivo se puede compilar con el archivo fuente para crear una prueba ejecutable que refleje el testigo de violación.

Tenga en cuenta que si el testigo de violación no contiene suficiente información para crear una prueba ejecutable, el resultado de validación será ERROR y la salida de la consola contendrá la siguiente línea: Could not export a test harness, some test-vector values are missing.