Download Plug-In Development Guide - Frama-C

CHAPTER 5. REFERENCE MANUAL
9. Makefile Creation creates Makefile from Makefile including information provided
by this configuration.
10. Summary displays summary of each plug-in availability.
5.3
Makefiles
In this section, we detail the organization of the different Makefiles existing in Frama-C. First
Section 5.3.1 presents a general overview. Next Section 5.3.2 details the different sections
of Makefile.config.in, Makefile.common, Makefile.generic and Makefile. Next Section 5.3.3 introduces the variables customizing Makefile.plugin and Makefile.dynamic.
Finally Section 5.3.4 shows specific details of Makefile.dynamic.
5.3.1
Overview
Frama-C uses different Makefiles (plus the plug-in specific ones). They are:
• Makefile: the general Makefile of Frama-C;
• Makefile.generating: it contains the complex rules that generate files. It is not
directly in the general Makefile in order to reduce the dependencies of these rules to
Makefile.generating;
• Makefile.config.in: the Makefile configuring some general variables (especially the
ones coming from configure);
• Makefile.common: the Makefile providing some other general variables;
• Makefile.generic: the Makefile providing generic rules for compiling source files
• Makefile.plugin: the Makefile introducing specific stuff for plug-in compilation;
• Makefile.dynamic: the Makefile usable by plug-in specific Makefiles.
• Makefile.dynamic_config: this Makefile is automatically generated either from
Makefile.dynamic_config.internal or Makefile.dynamic_config.external. It
sets variables which automatically configure Makefile.dynamic.
• Makefile.kernel is automatically generated from Makefile. It contains several variables useful for linking a plug-in against the Frama-C kernel.
The first one is part of the root directory of the Frama-C distribution while the other ones
are are part of directory share. Each Makefile either includes or is included into at least
another one. Figure 5.6 shows these relationship. Makefile and Makefile.dynamic are
independent: the first one is used to compile the Frama-C kernel while the second one is used
to compile the Frama-C plug-ins. Their common variables are defined in Makefile.common
(which includes Makefile.config.in). They also include Makefile.generic, that defines
default compilation rules for various kinds of source files. Makefile.plugin defines generic
rules and variables for compiling plug-ins. It is used both by Makefile for kernel-specific
plug-ins integrated compiled from the Frama-C Makefile and by Makefile.dynamic for plugins with their own Makefiles.
98