When benchmarking Frama-C, consider option -no-autoload-plugins

When using Frama-C in a series of benchmarks or test suites, especially when they consist of several small programs, consider using -no-autoload-plugins for better performance. This post explains why it is useful, as well as its downsides.

Minimize startup time with -no-autoload-plugins

By default, running frama-c makes it load all of its plugins (over 30 on version 22 - Titanium), resulting in a non-negligible startup time: about 0.2 seconds on a fast laptop. For most uses of Frama-C, this is dwarfed by the execution time of the plugins themselves. However, when parsing hundreds or thousands of small test files (such as those in the Juliet test suite), this adds up. Adding option -no-autoload-plugins avoids this overhead, by charging no plugins at all. This option is best combined with the explicit loading of the plugins that are of interest to you, via option -load-module, followed by the plugin module names.

For instance, to run Eva, the following list of plugins is sufficient in most cases:

frama-c -no-autoload-plugins -load-modules eva,scope,variadic <other options, filenames, etc.>

Note: when -no-autoload-plugins is set, some plugin dependencies are not loaded. This may result in failures when functions are requested from other plugins; usually, running the analysis on a few examples is enough to detect such cases, and the error message provides hints about which plugins are missing. Here’s a brief explanation why the above plugins are useful in conjunction with Eva:

• scope: this plugin is used by Eva at the end of an analysis, when removing (syntactically) redundant alarms, unless option -eva-no-remove-redundant-alarms is used;
• variadic: during parsing, the Variadic plugin instantiates calls to variadic functions such as printf and scanf, adding ACSL specifications. Without Variadic, Eva will raise warnings when these functions are called.

This usage of -no-autoload-plugins is present in several of Frama-C’s non-regression test suites, as well as in some open source case studies composed of several small tests (e.g. cerberus).

Finding Frama-C module names to use with -load-module

By giving Frama-C plugin names to -load-module, you can load the plugins you need for your specific analysis, but you must know its module name. This is often the plugin’s short name, that is, the prefix of its options, which you can consult via frama-c -plugins. For instance, Eva’s module name is eva, InOut’s is inout, etc. Only a few plugins do not follow this rule, mostly for historic reasons:

• Markdown report’s module name is markdown_report, instead of mdr;
• RTE’s module name is rtegen, instead of rte;
• Semantic constant folding is constant_propagation, instead of scf;
• Loop Analysis (deprecated) is loopanalysis and not loop;
• Callgraph is callgraph, not cg.

Overall, just remember that OCaml module names cannot contain hyphens - nor spaces, only underscores.

Also, note that the actual name of these module is prefixed by frama-c-, but -load-module automatically tries adding the prefix when it does not find another module with the same name. Thus you can use -load-module frama-c-eva instead of -load-module eva, for instance.

Conclusion

Frama-C’s default configuration is optimized for typical analysis tasks and easier plugin integration; however, when running benchmarks with thousands of small files, using -no-autoload-plugins and manually selecting plugins via -load-module is a more efficient approach.

When running any kind of benchmarks or large-scale comparison between Frama-C and other tools, do not hesitate to contact us; we may be able to provide usage tips to help you get faster results, and we are always interested in seeing how people use Frama-C.