Este es el comando goto-cc que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
cbmc - Verificador de modelo acotado para programas C / C ++ y Java
SINOPSIS
cbmc [--propiedad ID de propiedad] archivo.c ...
cbmc [--mostrar-propiedades] archivo.c ...
cbmc [--todas-propiedades] archivo.c ...
ir a cc [-YO incluir-ruta] [-C] archivo.c [-o archivoout.o]
goto-instrumento en archivo archivar
Aquí solo se enumeran las opciones más útiles; vea a continuación el resto.
DESCRIPCIÓN
cbmc genera rastros que demuestran cómo se puede violar una afirmación, o prueba que
la aserción no se puede violar dentro de un número determinado de iteraciones de bucle. CBMC puede leer
código fuente directamente, o un goto-binary generado por goto-cc. Los programas Java se dan como
archivos de clase. Sin más opciones, cbmc comprueba todas las propiedades (automáticamente
generado o especificado por el usuario) que se encuentran en el programa. Si alguna de las propiedades puede ser
violado, se imprime un contraejemplo y se cancela el análisis. El análisis puede ser
restringido a una propiedad en particular con la opción --property. El resultado de la verificación
para todas las propiedades se puede obtener mediante la opción --all-properties.
ir a cc lee el código fuente y genera un goto-binary. Su interfaz de línea de comandos es
diseñado para imitar el de gcc(1). Tenga en cuenta en particular que ir a cc distingue entre
compilar y vincular fases, tal como lo hace gcc. cbmc espera un goto-binary para el cual
se ha completado la vinculación.
goto-instrumento lee un goto-binary, realiza una transformación de programa dada, y luego
escribe el programa resultante como goto-binary en el disco.
El flujo habitual es (1) traducir la fuente a un goto-binary usando goto-cc, luego (2)
realizar la instrumentación con goto-instrument, y finalmente (3) realizar el análisis con
cbmc.
CAMPUS
FRONTEND CAMPUS (cbmc y ir a cc)
-Yo camino
Establecer ruta de inclusión (C / C ++)
-Dmacro
Definir macro de preprocesador (C / C ++)
--preproceso
Detener después del preprocesamiento
--mostrar-tabla-de-símbolos
Mostrar tabla de símbolos
--show-goto-funciones
Mostrar programa ir a
ARQUITECTÓNICO CAMPUS (cbmc y ir a cc)
cbmc de forma predeterminada, utiliza configuraciones arquitectónicas que coinciden con las de la máquina cbmc is
ejecutado, es decir, las configuraciones a continuación solo son necesarias para verificar el software que está
destinado a ejecutarse en una arquitectura o sistema operativo diferente. ir a cc genera un goto-binario para un
arquitectura particular, es decir, la arquitectura no se puede cambiar después de que el goto-binario es
generado.
--16, --32, --64
Establecer ancho de int
--LP64, --ILP64, --LLP64, --ILP32, --LP32
Establecer ancho de int, long y pointers
- little-endian
Permitir conversiones de bytes de palabras en little-endian
--big-endian
Permitir conversiones de bytes de palabras en big endian
- carácter no firmado
Hacer "char" sin firmar de forma predeterminada
--arch Establecer arquitectura de destino
--os Establecer el sistema operativo de destino
--no arco
No configure una arquitectura
--no-biblioteca
Deshabilitar la biblioteca C abstracta incorporada
--redondeo al más cercano, --redondo a más inf, --redondo a menos-inf, --redondeo a cero
Modo de redondeo de punto flotante IEEE para usar cuando comienza el programa (el predeterminado es round
al más cercano). El programa bajo verificación puede anular esta configuración, por ejemplo, con
gordo(3).
PROGRAMA INSTRUMENTACIÓN CAMPUS (cbmc y goto-instrumento)
Ambos cbmc y goto-instrumento puede generar afirmaciones que detectan errores comunes específicos,
como se indica a continuación.
- verificación de límites
Habilitar comprobaciones de límites de matriz
--div-por-cero-comprobación
Habilitar la división por cheques cero
- comprobación de puntero
Habilitar comprobaciones de puntero
--firmado-desbordamiento-control
Habilitar comprobaciones aritméticas de desbordamiento y subdesbordamiento para aritmética de enteros con signo
- verificación de desbordamiento sin firmar
Habilite las comprobaciones aritméticas de desbordamiento y subdesbordamiento para aritmética de enteros sin signo
--nan-cheque
Verifique los cálculos de punto flotante para NaN
--no-aserciones
Ignorar las afirmaciones proporcionadas por el usuario
- sin supuestos
Ignore las suposiciones proporcionadas por el usuario
- etiqueta de etiqueta de error
Verifique que la etiqueta dada sea inalcanzable
PROGRAMA INSTRUMENTACIÓN CAMPUS (goto-instrumento solamente)
goto-instrumento admite transformaciones de programas más complejas.
- no volátil
Hace lecturas de variables volátiles no deterministas
- función isr
Instrumenta una rutina de servicio de interrupción con el nombre dado
- E / S mapeadas en memoria de mmio Instruments
--nodet-estático
Las variables con vida útil estática se inicializan de forma no determinista
--volcado-c
Genere código fuente ANSI-C en lugar de goto binario.
BMC CAMPUS (cbmc)
--todas-propiedades
Informar el estado de todas las propiedades
--mostrar-propiedades
Mostrar solo propiedades
--show-bucles
Mostrar los bucles en el programa
--afirmaciones-encubiertas
Compruebe qué afirmaciones son accesibles
--nombre de la función
Establecer el nombre de la función principal
- ID de propiedad
Solo verifique la propiedad específica con el identificador dado
- solo programa
Mostrar solo la expresión del programa
--profundidad nr
Limitar la profundidad de búsqueda
--nr viento
Relájese bucles nr veces
- puesta de sol L: B, ...
Desenrolle el bucle L con un límite de B (use --show-loops para obtener los ID del bucle)
--mostrar-vcc
Mostrar las condiciones de verificación
- fórmula de rebanada
Eliminar asignaciones no relacionadas con la propiedad
--afirmaciones-sin-desenrollar
No genere afirmaciones de desenrollamiento
--sin nombres bonitos
No simplifique los identificadores
BACKEND CAMPUS (cbmc)
--dimacs
Genere CNF en formato DIMACS para su uso por solucionadores SAT externos
embellecer codicioso
Embellecer el contraejemplo (heurística codiciosa)
--smt1 Subobjetivos de salida en sintaxis SMT1 (experimental)
--smt2 Subobjetivos de salida en sintaxis SMT2 (experimental)
--boolector
Usar boolector (experimental)
--mathsat
Usar MathSAT (experimental)
--cvc Usa CVC3 (experimental)
--yice
Utilice Yices (experimental)
--z3 Usa Z3 (experimental)
--refinar
Usar procedimiento de refinamiento (experimental)
--outfile nombre de archivo
Fórmula de salida al archivo dado
--arreglos-uf-nunca
Nunca convierta matrices en funciones no interpretadas
--matrices-uf-siempre
Convierta siempre las matrices en funciones no interpretadas
MEDIO AMBIENTE
Todas las herramientas respetan la variable de entorno TMPDIR al generar archivos temporales y
directorios. Además, tenga en cuenta que el preprocesador utilizado por CBMC utilizará el entorno
variables para localizar archivos de encabezado. GOTO-CC tiene como objetivo aceptar todas las variables de entorno que
GCC lo hace.
DERECHOS DE AUTOR
2001-2014, Daniel Kroening, Edmund Clarke
Use goto-cc en línea usando los servicios de onworks.net
