Search code examples
frama-c

Getting quick help information for Frama-C


How to get quick help information for Frama-C (without having to resort to the manuals)? Typing "frama-c -help" displays very little useful data.


Solution

  • Here is a list of useful quick commands to obtain help, or to improve verbose/debug information when running frama-c:

    • frama-c -kernel-help: the "actual" help page of the Frama-C kernel, with lots of useful options;
    • man frama-c: very similar results to frama-c -kernel-help;
    • frama-c -kernel-msg-key help: displays all message categories known by the kernel, used to produce verbose and debugging messages. They have no associated description, but a few are self-explanatory. For instance, -kernel-msg-key pp shows the actual preprocessing command used by Frama-C when parsing files;
    • frama-c -kernel-warn-key help: lists all warning categories, plus their status (active, inactive, treat as error, abort immediately, warn once, etc);
    • frama-c -machdep help: lists all available architectures known by Frama-C.

    Each plug-in has its own <plugin>-help, <plugin>-msg-key and <plugin>-warn-key. It may also have extra "listing" options. For instance, the Eva (value analysis) plugin has option -val-builtins-list, which lists all available Eva built-ins and which function names are mapped to them.