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.
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
CaFE uses Eva internally to compute an over-approximation of the states of the program.