Download Plug-In Development Guide - Frama-C

4.7. PLUG-IN GENERAL SERVICES
MACRO: macro-name content
where macro-name is any sequence of characters containing neither a blank nor an @, and
content extends until the end of the line. Once such a directive has been encountered,
each occurrence of @macro-name@ in a CMD, OPT, STDOPT or EXECNOW directive at this
configuration level or in any level below it will be replaced by content. Existing predefined macros are listed in section 5.4.1.
• The FILEREG directive contains a regular expression indicating which files in the directory containing the current test suite are actually part of the suite. This directive is
only usable in a test_config configuration file.
4.7
Plug-in General Services
Module Plugin provides an access to some general services available for all plug-ins. The
goal of this module is twofold. First, it helps developpers to use general Frama-C services.
Second, it provides to the end-user a set of features common to all plug-ins. To access to
these services, you have to apply the functor Plugin.Register.
Each plug-in must apply this functor exactly once.
Example 4.9 Here is how the plug-in From applies the functor Plugin.Register for its own
use.
include Plugin.Register
(struct
let name = "from analysis"
let shortname = "from"
let help = "functional dependencies"
end)
Applying this functor mainly provides two different services. First it gives access to functions
for printing messages in a Frama-C-compliant way (see Section 4.8). Second it allows to define
plug-in specific parameters available as options on the Frama-C command line to the end-user
(see Section 4.13).
4.8
Logging Services
Displaying results of plug-in computations to users, warning them of the hypothesis taken by
the static analyzers, reporting incorrect inputs, all these tasks are easy to think about, but
turn to be difficult to handle in a readable way. As soon as your plug-in is registered (see
Section 4.7 above), though, you automatically benefit from many logging facilities provided
by the kernel. What is more, when logging through these services, messages from your plug-in
combine with other messages from other plug-ins, in a consistent and user-friendly way.
As a general rule, you should never write to standard output and error channels through
OCaml standard libraries. For instance, you should never use Pervasives.stdout and
Pervasives.stderr channels, nor Format.printf-like routines.
53