CaFE

Overview

CaFE (CaRet Frama-C Extension) is a small model-checker dedicated to prove CaRet properties over C programs. CaRet is “a temporal logic of nested calls and returns”, i.e. a flavor of temporal logic well suited to describe a program’s call stack.

Usage

CaFE is available as a separate open-source plug-in. Once installed, it will be activated by the -cafe option, while -cafe-formula allows specifying the file in which to formula to be verified lies. A typical command will thus be the following:

frama-c -cafe file.c -cafe-formula file.caret

Dependencies

CaFE uses Eva internally to compute an over-approximation of the states of the program.