En este práctico vamos a descubrir unas funcionalidades de CBMC, una herramienta que puede ser usada para ejecutar una verificación acotada (bounded model checking) directamente sobre código C. Permite al usuario averiguar directamente ciertas aserciones, pero también puede averiguar si hay problemas potenciales con punteros y límites de índices de arreglos. También puede verificar ciertas partes de un código sin borrar otras partes. Por supuesto, como lleva a cabo un model checking acotado, tiene problemas cuando se encuentra con bucles infinitos, pero también es capaz de limitar la cantidad de veces que se repite un bucle, e incluso detectar si se pierde algun comportamiento haciéndolo (es decir, si el bucle infinito no era realmente infinito).
Encontrarás más detalles sobre CBMC en el manual, la página del proyecto, o la documentación de la API.
En este práctico de laboratorio, se tratará de ver un pantallazo de las funcionalidades básicas de CBMC con el objetivo de entender su comportamiento y salida. Si lo terminás, te recomiendo de verificar tu propio código C.
cbmc file.c
. ¿Qué ocurre?cbmc file.c --show-claims
te muestra todos los claims (afirmaciones, aserciones) que CBMC intenta verificar (con nombre y detalles).cbmc file.c --claim main.assertion.1
te permite averiguar una sola aserción.--show-vcc
. Si agregás la opción --slice-formula
, solo te mostrará las restricciones que son relevantes para cada aserción (tal vez es más fácil de leer).__CPROVER_assume
? ¿Qué pasa si la sacás?cbmc tableau.c
. ¿Qué pasa?--bounds-check
. ¿Qué pasa si lo hacés?--bounds-check
). ¿Qué ocurre?--pointer-check
. Utilizala.--unwind n
. Ejecutá cbmc boucle.c --unwind 3
. ¿Qué ocurre? ¿Porqué?--unwinding-assertions
. Ejecutá cbmc boucle.c --unwind 3 --unwinding-assertions
. ¿Qué ocurre? ¿Para qué valor de unwind
obtenés el comportamiento deseado?--function
. En ese caso, va a fijar el punto de entrada en la función que pasás como argumento. Ejecutá cbmc boucle.c --function boucle
. ¿Qué ocurre?--unwind
. ¿Es mejor?--unwinding-assertions
. ¿Funciona? ¿Porqué? ¿Podés encontrar un valor de unwind
para lo cual funciona?__CPROVER_assume
, ¿podés tener una verificación exitosa?unwind
para lo cual la verificación es exitosa y ningun comportamiento se escapa (es decir --unwinding-assertions
no produce ninguna falla)?--pointer-check
. ¿Porqué hay un error? ¿Podés poner una restricción sobre n
tal que la verificación sea exitosa?queue_test
. ¿Hay un error? No te olvides de las opciones --bounds-check
y --pointer-check
.Verificá la versión de CBMC que tenés instalada ejecutando cbmc
sin opciones ni archicos.
Si tu versión es 5.6
, cbmc
no muestra los contraejemplos (si hay) por defecto, hay que darle la opción --trace
.