4. Verification Tool

Overview

This command-line verification tool utilizes CIL plugins described on the previous page. The tool is written in Typescript and runs on ts-node by default (Can also be compiled to JS for performance reasons). The files are located in cli/.

The program takes a single C file and will try to prove it with CBMC incrementally, leading to quicker results. The tool starts with the innermost extracted function containing an assertion, moving to the callee when failing.

WARNING: If you have a function containing CBMC assertions that cannot be proved on its own, and is called in multiple functions within your program, you have to test it with one caller at a time. This is because the tool will not know which caller to go to when CBMC fails to prove the function.

Usage

make extractMLC
make findFuncs
npm run verify -- --file <filename.c>

See getting started for installation details.

Note: You have to define CPROVER CBMC functions in your file, otherwise CIL will complain and fail. Defining them with empty bodies will not affect CBMC.

The program will output a JSON array for every function containing assertions. The functions that were originally present in the program will be labelled by their names, extracted functions will be labelled by the line of code of the root of the cycle from which they were extracted.

isTrue variable denotes whether the segment could be proved provedAt Is set to the minimal* function (or line of code of a cycle - see above) where the assertions could be proved.

* minimal denotes the innermost cycle/loop, i.e. the one closest to the assertion(s)