Frama-C:
Plug-ins:
Libraries:

Frama-C API

This is the API documentation of Frama-C. Use the side menu for accessing the different parts of the API. Please refer to the plug-in development guide for a detailed tutorial on how to develop Frama-C plug-ins.

The main entry point to consider is the Frama-C Kernel.

Simple plug-in tutorial

This short tutorial is the first part provide the first part of the tutorial section available in the plug-in development guide. It illustrates the creation of a simple plug-in, and how to test and document it.

A Frama-C plug-in built using Dune is composed minimally of the following files:

  • a dune-project file that describes the project,
  • a dune file that describes the build of the project
  • a <my_plugin>.ml file that defines the API of the plug-in (which can be empty).

For example, for the Hello plug-in:

./dune-project

(lang dune 3.7)
(using dune_site 0.1)
(name frama-c-hello)
(package (name frama-c-hello))

./dune

(library
 (name Hello)
 (public_name frama-c-hello.core)
 (flags -open Frama_c_kernel :standard)
 (libraries frama-c.kernel))

(plugin
 (optional)
 (name hello)
 (libraries frama-c-hello.core)
 (site (frama-c plugins)))

./hello.ml is just an empty file.

Then the plugin can be built using the following command:

dune build

If Dune is installed, this should compile the project successfully. Note that Dune emits messages during compilation, but erases them afterwards. In case of success, there will be no visible output at the end. Note that this behavior can be configured with Dune’s option --display.

Dune always looks for dune-project files in the parent directories, so make sure that your Hello directory is not inside another one containing a Dune project (e.g. if you are running this directly from the Frama-C source archive), otherwise dune build may fail. You can always add option --root, or create an empty dune-workspace file in the current directory to force Dune to ignore parent directories.

Note a few details about the naming conventions:

  • in the dune-project file, the name of the plugin is frama-c-<my-plugin>
  • in the dune file, the name of:
    • the library is my_plugin;
    • the public name of the library is frama-c-<my-plugin>.core (dune project name core);
    • the name of the plugin is <my-plugin>;
    • the plugin must at least include the library frama-c-<my-plugin>.core.

Of course, for now, our plug-in does nothing, so let us change that.

A Very Simple Plug-in

Let us add a simple file to our plug-in:

./hello_world.ml

let run () =
  try
    let chan = open_out "hello.out" in
    Printf.fprintf chan "Hello, world!\n";
    flush chan;
    close_out chan
  with Sys_error _ as exc ->
    let msg = Printexc.to_string exc in
    Printf.eprintf "There was an error: %s\n" msg

let () = Db.Main.extend run

This file defines a simple function that writes a message to an output file, then registers the function run as an entry point. Frama-C will call it among the other plug-in entry points if the plug-in is loaded.

The plug-in is compiled the same way as previously explained. Then, one can execute the script using the command:

dune exec -- frama-c

Executing this command creates a hello.out file in the current directory.

You can think of dune exec -- as a wrapper for frama-c which adds your plug-in to those already present in Frama-C. It operates on a local Dune sandbox, allowing you to test it without risking “polluting” your installed Frama-C.

Registering a Plug-in in Frama-C

To make this script better integrated into Frama-C, its code must register itself as a plug-in. Registration provides general services, such as outputting to the Frama-C console and extending Frama-C with new command-line options.

Registering a plug-in is achieved through the use of the Plugin.Register functor:

./hello_world.ml

let help_msg = "output a warm welcome message to the user"

module Self = Plugin.Register
    (struct
      let name = "hello world"
      let shortname = "hello"
      let help = help_msg
    end)

let run () =
  try
    let chan = open_out "hello.out" in
    Printf.fprintf chan "Hello, world!\n";
    flush chan;
    close_out chan
  with Sys_error _ as exc ->
    let msg = Printexc.to_string exc in
    Printf.eprintf "There was an error: %s\n" msg

let () = Db.Main.extend run

The argument to the Plugin.Register functor is a module with three values:

  • name is an arbitrary, non-empty string containing the full name of the module.
  • shortname is a small string containing the short name of the module, to be used as a prefix for all plug-in options. It cannot contain spaces.
  • help is a string containing free-form text, with a description of the module.

Visible results of the registration include:

  • “hello world” appears in the list of available plug-ins; you can check it by running dune exec -- frama-c -plugins;
  • default options for the plug-in work, including the inline help (available with dune exec -- frama-c -hello-help).

Displaying Messages

The signature of the module Self obtained by applying Plugin.Register is General_services. One of these general services is logging, i.e. message display. In Frama-C, one should never attempt to write messages directly to stderr or stdout: use the general services instead.

let help_msg = "output a warm welcome message to the user"

module Self = Plugin.Register
    (struct
      let name = "hello world"
      let shortname = "hello"
      let help = help_msg
    end)

let run () =
  Self.result "Hello, world!";
  let product =
    Self.feedback ~level:2 "Computing the product of 11 and 5...";
    11 * 5
  in
  Self.result "11 * 5 = %d" product

let () = Db.Main.extend run

Running this script yields the following output:

$ dune exec -- frama-c
[hello] Hello, world!
[hello] 11 * 5 = 55

The result routine is the function to use to output results of your plug-in. The Frama-C output routines take the same arguments as the OCaml function Format.printf.

Function feedback outputs messages that show progress to the user. In this example, we decided to emit a feedback message with a log level of 2, because we estimated that in most cases the user is not interested in seeing the progress of a fast operation (simple multiplication). The default log level is 1, so by default this message is not displayed. To see it, the verbosity of the hello plug-in must be increased:

$ dune exec -- frama-c -hello-verbose 2
[hello] Hello, world!
[hello] Computing the product of 11 and 5...
[hello] 11 * 5 = 55

For a comprehensive list of logging routines and options, refer to the plug-in development guide.

Adding Command-Line Options

We now extend the hello world plug-in with new options.

If the plug-in is installed (globally, with dune install, or locally, with dune exec), it will be loaded and executed on every invocation of frama-c, which is not how most plug-ins work. To change this behavior, we add a boolean option, set by default to false, that conditionally enables the execution of the main function of the plug-in. The usual convention for the name of this option is the short name of the module, without suffix, i.e. -hello in our case.

We also add another option, -hello-output, that takes a string argument. When set, the hello message is displayed in the file given as argument.

let help_msg = "output a warm welcome message to the user"

module Self = Plugin.Register
    (struct
      let name = "hello world"
      let shortname = "hello"
      let help = help_msg
    end)

module Enabled = Self.False
    (struct
      let option_name = "-hello"
      let help = "when on (off by default), " ^ help_msg
    end)

module Output_file = Self.String
    (struct
      let option_name = "-hello-output"
      let default = "-"
      let arg_name = "output-file"
      let help =
        "file where the message is output (default: output to the console)"
    end)

let run () =
  try
    if Enabled.get() then
      let filename = Output_file.get () in
      let output msg =
        if Output_file.is_default() then
          Self.result "%s" msg
        else
          let chan = open_out filename in
          Printf.fprintf chan "%s\n" msg;
          flush chan;
          close_out chan;
      in
      output "Hello, world!"
  with Sys_error _ as exc ->
    let msg = Printexc.to_string exc in
    Printf.eprintf "There was an error: %s\n" msg

let () = Db.Main.extend run

Registering these new options is done by calling the Self.False and Self.String functors, which respectively create a new boolean option whose default value is false and a new string option with a user-defined default value (here, "-"). The values of these options are obtained via Enabled.get () and Output_file.get ().

With this change, the hello message is displayed only if Frama-C is executed with the -hello option.

$ dune exec -- frama-c
$ dune exec -- frama-c -hello
[hello] Hello, world!
$ dune exec -- frama-c -hello -hello-output hello.out
$ ls hello.out
hello.out

These new options also appear in the inline help for the hello plug-in:

$ dune exec -- frama-c -hello-help
...
***** LIST OF AVAILABLE OPTIONS:

-hello              when on (off by default), output a warm welcome message
                    to the user (opposite option is -no-hello)
-hello-output <output-file>  file where the message is output (default:
                    output to the console)
...

About the plug-in build process

As mentioned before, each plug-in needs a module declaring its public API. In our examples, this was file hello.ml, which was left empty. To make it more explicit to future users of our plug-in, it is customary to add a comment such as the following:

./hello.ml

(** Hello World plug-in.

    No function is exported. *)

Note that, to avoid issues, the name of each compilation unit (here hello_world) must be different from the plug-in name set in the dune file (here hello), from any other plug-in names (e.g. eva, wp, etc.) and from any other Frama-C kernel OCaml files (e.g. plugin).

The module name chosen by a plug-in (here hello) is used by Dune to pack that plug-in; any functions declared in it become part of the plug-in’s public API. They become accessible to other plug-ins and need to be maintained by the plug-in developer. Leaving it empty avoids exposing unnecessary implementation details.

Inside the plug-in’s directory, dune build compiles it and creates the packed module. It can be installed along with the other Frama-C plug-ins using dune install.

You can then just launch frama-c (without any options), and the hello plug-in will be automatically loaded. Check it with the command frama-c -hello-help.

You can uninstall it by running dune uninstall.

Splitting your source files

Here is a slightly more complex example where the plug-in has been split into several files. Usually, plug-in registration through Plugin.Register should be done at the bottom of the module hierarchy, while registration of the run function through Db.Main.extend should be at the top. The three following files completely replace the ./hello_world.ml from the previous section. Modules are directly called by their name in the classical OCaml way.

./hello_options.ml

let help_msg = "output a warm welcome message to the user"

module Self = Plugin.Register
    (struct
      let name = "hello world"
      let shortname = "hello"
      let help = help_msg
    end)

module Enabled = Self.False
    (struct
      let option_name = "-hello"
      let help = "when on (off by default), " ^ help_msg
    end)

module Output_file = Self.String
    (struct
      let option_name = "-hello-output"
      let default = "-"
      let arg_name = "output-file"
      let help =
        "file where the message is output (default: output to the console)"
    end)

./hello_print.ml

let output msg =
  try
    let filename = Hello_options.Output_file.get () in
    if Hello_options.Output_file.is_default () then
      Hello_options.Self.result "%s" msg
    else
      let chan = open_out filename in
      Printf.fprintf chan "%s\n" msg;
      flush chan;
      close_out chan
  with Sys_error _ as exc ->
    let msg = Printexc.to_string exc in
    Printf.eprintf "There was an error: %s\n" msg

./hello_run.ml

let run () =
  if Hello_options.Enabled.get() then
    Hello_print.output "Hello, world!"

let () = Db.Main.extend run

The plug-in can be tested again by running:

$ dune build
$ dune install
<...>
$ frama-c -hello -hello-output hello.out
$ more hello.out
Hello, world!

However, this does not consist in a proper test per se. The next section presents how to properly test plug-ins.

Testing your Plug-in

Frama-C supports non-regression testing of plug-ins. This is useful to check that further plug-in modifications do not introduce new bugs. The tool allowing to perform the tests is called Ptests.

Historically, ptests was developed before Frama-C used Dune. It was adapted to Dune to maintain backwards compatibility, but new plug-ins may prefer using Dune’s test system directly.

This is the general layout of the tests directory in a Frama-C plug-in; each file will be explained later.

<plug-in directory>
+- tests
   +- ptests_config
   +- test_config
   +- suite1
      +- test1.c
      +- ...
      +- oracle
         +- test1.res.oracle
         +- test1.err.oracle
         +- ...
      +- result
         +- test1.0.exec.wtests
         +- ...
  +- ...

Inside the tests directory, ptests_config lists the test suites, i.e. directories containing tests.

./tests/ptests_config

DEFAULT_SUITES= hello

Small plug-ins typically have a single test directory with the plug-in name.

Then, a default configuration must be provided for the tests. This is done by adding a test_config file to the tests directory.

./tests/test_config

PLUGIN: hello

This configuration must include the plug-ins required by the test; usually, the plug-in itself, but also other plug-ins on which it depends. The plug-in name is the one provided in the plugin section of the dune file.

For non-regression testing, the current behavior of a program is taken as the oracle against which future versions will be tested. In this tutorial, the test will be about the correct Hello, world! output made by the option -hello of the plug-in.

Each test file should contain a run.config comment with test directives and the C source code used for the test.

For this tutorial, no actual C code is needed, so ./tests/hello/hello_test.c will only contain the run.config header:

./tests/hello/hello_test.c

/* run.config
   OPT: -hello
 */

In this file, there is only one directive, OPT: -hello, which specifies that Frama-C will set option -hello when running the test.

Once run.config has been configured, it becomes possible to generate Dune test files via the Ptests tool:

$ frama-c-ptests
Test directory: tests
Total number of generated dune files: 2

This must be done each time a test configuration is modified or a test file or directory is added.

Then, one can execute the tests and get the output generated by the plug-in, by running dune build @ptests. Note that if you forget the intermediate step of running frama-c-ptests, you may end up with the following error:

Error: Alias "ptests" specified on the command line is empty.
It is not defined in tests or any of its descendants.

But with the dune files generated by frama-c-ptests, you can run the tests:

$ dune build @ptests
Files ../oracle/hello_test.res.oracle and hello_test.res.log differ
% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
(cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log"
"../oracle/hello_test.res.oracle")
File "tests/hello/oracle/hello_test.res.oracle", line 1, characters 0-0:
diff --git a/_build/default/tests/hello/oracle/hello_test.res.oracle
            b/_build/default/tests/hello/result/hello_test.res.log
index e69de29..5f6ab23 100644
--- a/_build/default/tests/hello/oracle/hello_test.res.oracle
+++ b/_build/default/tests/hello/result/hello_test.res.log
@@ -0,0 +1,2 @@
+[kernel] Parsing hello_test.c (with preprocessing)
+[hello] Hello, world!

There is a lot of information in the output. The relevant parts can be summarized as:

  • Dune runs its tests inside a sandboxed environment, in directory _build/default, which is (approximately) a copy of the plug-in file tree;
  • Dune compared two files, none of which existed before running the test: result/hello_test.res.log and oracle/hello_test.res.oracle;
  • The last lines (which should be colored, if your terminal supports colors) show the textual difference between the expected and actual outputs.

The first file, result/hello_test.res.log, is the actual output of the execution of the test command. The second file, oracle/hello_test.res.oracle, is the expected output of the test.

The result file is re-generated each time the test is run. The oracle file, however, is supposed to exist beforehand (unless the test produces no output).

In reality, there are 2 pairs of files for each test: a pair .res.{log,oracle} and another .err.{log,oracle}. The first one contains results sent to the standard output (stdout), while the second one contains messages sent to the standard error (stderr). In our example, the error output is empty, so it generates no differences. Note that Dune only outputs messages in case of errors, i.e. tests producing the expected result are silent.

Finally, concerning the actual diff in the test (last two lines), the first line (starting with [kernel]) is emitted by the Frama-C kernel, and the second one is our plug-in’s result, as expected.

Once you have verified the actual output is the one you expected, you can promote it to the status of “official oracle” for future non-regression tests, by running:

$ dune promote

Note, however, that if the oracles do not exist, they must be created:

$ frama-c-ptests -create-missing-oracles tests
$ dune promote

The option -create-missing-oracles always creates both result and error oracles. Most of the time, however, only the former is useful. After promoting tests, it is useful to remove empty oracles:

$ frama-c-ptests -remove-empty-oracles tests

The new oracle should be committed to source control, for future testing.

Once your plug-in has test files, the dune build command presented earlier will not only compile your plug-in, but also run its tests. Therefore, if you want to simply compile it, you will have to run dune build @install instead. Despite the name, the command will not install your plug-in, it will only build and collect all files necessary for its installation.

Now, let’s introduce an error. Assume the plug-in has been modified as follows:

./hello_run.ml

let run () =
  if Hello_options.Enabled.get() then
    Hello_print.output "Hello world!" (* removed comma *)

let () = Db.Main.extend run

We assume that “Hello, world!” has been unintentionally changed to “Hello world!”. Running these commands:

$ dune build @install
<...>
$ dune build @ptests
Files ../oracle/hello_test.res.oracle and hello_test.res.log are different
% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
 (cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log" "../oracle/hello_test.res.oracle")
File "tests/hello/oracle/hello_test.res.oracle", line 1, characters 0-0:
diff --git a/_build/default/tests/hello/oracle/hello_test.res.oracle b/_build/default/tests/hello/result/hello_test.res.log
index 5f6ab2389a..cf2e5c010c 100644
--- a/_build/default/tests/hello/oracle/hello_test.res.oracle
+++ b/_build/default/tests/hello/result/hello_test.res.log
@@ -1,2 +1,2 @@
 [kernel] Parsing hello_test.c (with preprocessing)
-[hello] Hello, world!
+[hello] Hello world!

displays the differences (à la diff) between the current execution and the saved oracles. Here, the diff clearly shows that the only difference is the missing comma in the generated message due to our (erroneous) modification. After fixing the OCaml code, running again the previous commands shows that all test cases are successful.

You may check other Frama-C plug-ins as examples of how to integrate a plug-in with Ptests. Small plug-ins such as Report and Variadic are good examples (see directories src/plugins/report/tests and src/plugins/variadic/tests). Please note Frama-C offers no particular support for other kinds of testing purposes, such as test-driven development (TDD).

Summary of Testing Operations

Here’s a summarized list of operations in order to add a new test:

  1. Create a test case (.c or .i file in tests/<suite>).
  2. Add a run.config header to the test.
  3. frama-c-ptests -create-missing-oracles
  4. dune build @ptests
  5. Manually inspect oracle diffs to check that they are ok.
  6. dune promote
  7. frama-c-ptests -remove-empty-oracles

Operations to perform when modifying the plug-in code:

  1. dune build @install
  2. dune build @ptests
  3. If there are expected diffs, run dune promote; otherwise, fix code and re-run the first steps.

Documenting your Source Code

One can generate the documentation of a plugin using the command:

dune build @doc

This relies on Odoc and requires the plug-in to be documented following the Odoc guidelines.

We show here how the Hello plug-in could be slightly documented and use Odoc features such as @-tags and cross-references. First, we modify the hello.ml file to export all inner modules, otherwise Odoc will not generate documentation for them:

./hello.ml

(** Hello World plug-in.
    All modules are exported to illustrate documentation generation by odoc. *)

module Hello_run = Hello_run
module Hello_options = Hello_options
module Hello_print = Hello_print

Then, we add some documentation tags to our modules:

./hello_options.ml

(** This module contains the possible command line options
    for the Hello plug-in.
    @author Anne Onymous
    @see <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>
        Frama-C Developer Manual, Tutorial
*)

(** Content of the welcome message. *)
let help_msg = "output a warm welcome message to the user"

(** Registration of the plug-in to Frama-C. *)
module Self = Plugin.Register
    (struct
      let name = "hello world"
      let shortname = "hello"
      let help = help_msg
    end)

(** Enabling of the plug-in. *)
module Enabled = Self.False
    (struct
      let option_name = "-hello"
      let help = "when on (off by default), " ^ help_msg
    end)

(** Output of the plug-in. *)
module Output_file = Self.String
    (struct
      let option_name = "-hello-output"
      let default = "-"
      let arg_name = "output-file"
      let help =
        "file where the message is output (default: output to the console)"
    end)

./hello_print.ml

(** This module contains the printing method of the Hello plug-in.
    @author Anne Onymous
    @see <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>
        Frama-C Developer Manual, Tutorial
*)

(** Outputs a message to the output selected in
        {!module:Hello_options.Output_file}.
    @param msg Message to output.
    @raise Sys_error if filesystem error.
*)
let output msg =
  try
    let filename = Hello_options.Output_file.get () in
    if Hello_options.Output_file.is_default () then
      Hello_options.Self.result "%s" msg
    else
      let chan = open_out filename in
      Printf.fprintf chan "%s\n" msg;
      flush chan;
      close_out chan
  with Sys_error _ as exc ->
    let msg = Printexc.to_string exc in
    Printf.eprintf "There was an error: %s\n" msg

./hello_run.ml

(** This module contains the main control logic of the Hello plug-in.
    @author Anne Onymous
    @see <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>
        Frama-C Developer Manual, Tutorial
*)

(** Controls the output of a given message by
        {!val:Hello_print.output} depending on the state of
        {!module:Hello_options.Enabled}.
*)
let run () =
  if Hello_options.Enabled.get() then
    Hello_print.output "Hello, world!"

(** Definition of the entry point of the hello plug-in. *)
let () = Db.Main.extend run

Running dune build @doc will generate documentation files in ./_build/default/_doc/_html. Open index.html in your browser and navigate to see them. Note that Odoc may report some warnings due to absence of annotation data for Frama-C’s modules:

Warning: Couldn't find the following modules:
  Frama_c_kernel Frama_c_kernel__Plugin

This should not prevent the generation of documentation for the library itself; but links to modules such as Enabled and Output_file} will not work.

Conclusion

This simple tutorial now comes to its end. It focused on the standard features of architectures and interfaces of Frama-C plug-ins. A companion archive hello.tar.gz is available. The plug-in development guide provides a lot more details about the development of Frama-C plug-ins.