Home

Plug-In development guide

1. Type Index varinfo vid compinfo ckey enuminfo ename typeinfo tname stmt sid logic_info 1_var_info lv_id logic_var lv_id fieldinfo fname and fcomp ckey Figure 5 2 Indices of AST nodes Last when using a copy visitor the actions see previous section SkipChildren and ChangeTo must be used with care i e one has to ensure that the children are fresh Otherwise the new AST will share some nodes with the old one Even worse in such a situation the new AST might very well be left in an inconsistent state with uses of shared node e g a varinfo for a function f in a function call which do not match the corresponding declaration e g the GFun definition of f When in doubt a safe solution is to use JustCopy instead of SkipChildren and ChangeDoChildrenPost x fun x gt x instead of ChangeTo x 5 14 6 Differences Between the Cil and Frama C Visitors As said in Section 5 14 2 vstmt and vglob should not be redefined Use vstmt_aux and vglob_aux instead Be aware that the entries corresponding to statements and globals in Frama C tables are considered more or less as children of the node In particular if the method returns ChangeTo action see Section 5 14 3 it is assumed that it has taken care of updating the tables accordingly which can be a little tricky when copying a file from a project to another one Prefer ChangeDoChildrenPost On the other hand a SkipChildren action implies that t
2. Chapter 4 Software Architecture Target readers beginners In this chapter we present the software architecture of Frama C First Section 4 1 presents its general overview Then we focus on three different parts e Section 4 2 introduces the API of Cil 17 seen by Frama C e Section 4 3 shows the organisation of the Frama C kernel and e Section 4 4 explains the plug in integration 4 1 General Description The Frama C platform provides services to ease e analysis and source to source transformation of big size C programs e addition of new plug ins and e plug ins collaboration In order to reach these goals Frama C is based on a software architecture with a specific design which is presented in this document and summarized in Figure 4 1 Mainly this architecture is separated in three different parts e Cil C Intermediate Language 17 extended with an implementation of the specification language ACSL ANSI ISO C Specification Language 1 This is the intermediate language upon which Frama C is based See Section 4 2 for details e The Frama C kernel It is a toolbox on top of Cil dedicated to static analyses It provides data structures and operations which help the developer to deal with the Cil AST Abstract Syntax Tree as well as general services providing an uniform set of features to Frama C See Section 4 3 for details e The Frama C plug ins These are analyses or source to source transformati
3. 12 Chapter 2 Tutorial Target readers beginners This chapter aims at helping a developer to write his first Frama C plug in At the end of the tutorial any developer should be able to extend Frama C with a simple analysis available as a Frama C plug in This chapter was written as a step by step explanation on how to proceed towards this goal It will get you started but does not tell the whole story In particular some very important aspects for the integration in the framework are omitted here and are described in chapter 5 Section 2 1 explains the basis for writing a standard Frama C plug in while section 2 2 explains the basis for writing a plug in integrated with the Frama C kernel this is slightly more involved but allows deeper integration within the Frama C architecture You should do this only if you intend to contribute a large and very general purpose plug in to the community 2 1 Standard Plug in This section will teach you how to write the most basic plug in and run it from the Frama C toplevel Prerequisite To follow this tutorial e Frama C needs to be installed in your path e the Objective Caml compilers must be installed in your path These must be the same compilers as the ones you used to compile Frama C e GNU make must be in your path 2 1 1 Plug in Integration Overview Figure 2 1 shows how a plug in can integrate with the Frama C platform This tutorial focuses on specific parts of this fig
4. 5 4 Plug in Specific Makefile Prerequisite knowledge of make In this section we detail how to add a Makefile to a plug in Section 5 4 1 introduces how to write a Makefile for a given plug in thanks to Makefile dynamic while Section 5 4 2 explains how to integrate it in Makefile 5 4 1 Using Makefile dynamic In this section we detail how to write a Makefile for a given plug in Even if it is still possible to write such a Makefile from scratch Frama C provides a generic Makefile called Makefile dynamic which helps the plug in developer in this task This file is installed in the Frama C share directory So for writting your plug in specific Makefile you have to 1 set some variables for customizing your plug in 2 include Makefile dynamic 41 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT Example 5 4 A minimal Makefile is shown below That is the Makefile of the plug in Hello World presented in the tutorial see Section 2 1 2 Each variable set in this example has to be set by any plug in Example of Makefile for dynamic plugins LMP AHAAA AHAHAHAHAHAHAH IAIA AAAA III EEE N A A B B O a ES TUTTTAT ATTA AT AT ATID AT IT AT AT AT AT AT AT IT EEE ENT EN EEE EE ENERENEEEE EEE NET EE EEE EEE Frama c should be properly installed with make install before any use of this makefile FRAMAC_SHARE shell frama c byte print path FRAMAC_LIBDIR shell frama c byte print libpath PLUGIN_NAME Hello PLUG
5. The variable PLUGIN_NAME must hold a valid OCaml module name in particular it must be capitalized e PLUGIN_DIR is the directory containing the source file s for the plug in e PLUGIN_CMO is the list of the cmo files without the extension cmo nor the plug in path required to compile the plug in e PLUGIN_NO_TEST is set to yes because there is no specific test directory for the plug in see Section 2 2 6 about plug in testing Now we are ready to compile Frama C with the new plug in hello make At this point the plug in works properly a Frama C user can run the plug in safely bin toplevel byte hello Hello World 2 2 5 Connection with the Frama C World The plug in hello is now compiled but it is not fully registered within the Frama C framework In particular our plug in should be added in the plug in database Db in order to be simply used by other plug ins see Chapter 4 for details Extension of the Plug in Database For this purpose we have to extend Db with the new plug in hello File src kernel db mli 20 2 2 KERNEL INTEGRATED PLUG IN Hello World plug in see lt hello index html gt internal documentation module Hello sig val run Format formatter gt unit ref Print hello world x end File src kernel db ml module Hello struct let run mk fun Hello_world run end The interface declares a new module Hello containing a single function run Indeed run is a refe
6. These notions are summarized in Figure 5 1 One row contains the value of each data for a specific project and one line represents an internal state of a specific data Projects A Internal states FOR Project PA AST a value of a in p value of a in pn data di value of d in p value of d in Pn data dm value of dm in p value of dm in Pn Figure 5 1 Representation of the Frama C Internal State 5 11 2 Using Projects Actually Frama C maintains a current project Project current and a current AST Ast get which all operations are automatically performed on But sometimes plug in developers have to explicitly use them for example when the AST is modified usually through the use of a copy visitor see Section 5 14 or replaced e g if a new one is loaded from disk An AST must never be modified inside a project If such an operation is re quired you must either create a new project with a new AST usually by using File init_project_from_cil_file or File init_project_from_visitor or write the following line of code see Section 5 11 7 Project clear only Project Selection singleton Ast self Kind Only_Select_Dependencies O Operations over projects are grouped together in module Project A project has type Project t Function Project set_current sets the current project on which all operations are implicitly performed on the new current project Example 5 15 Suppose that you saved the cu
7. e Index fully new e Project new sub section Internal State Principle e Reference manual largely extended Software architecture fully new chapter Hydrogen 20080501 e First public release 98 1 2 a 3 lt a 4 ay 5 6 eatery 7 8 lt i 9 rs 10 11 12 13 BIBLIOGRAPHY Bibliography Patrick Baudin Jean Christophe Filli tre Thierry Hubert Claude March Benjamin Monate Yannick Moy and Virgile Prevosto ACSL ANSI C Specification Language April 2008 Patrick Baudin and Anne Pacalet Slicing plug in http frama c com slicing html Sylvain Conchon and Jean Christophe Filli tre Type Safe Modular Hash Consing In ACM SIGPLAN Workshop on ML Portland Oregon United States September 2006 Sylvain Conchon Jean Christophe Filli tre and Julien Signoles Designing a generic graph library using ML functors In Marco T Moraz n editor Trends in Functional Programming volume 8 of Trends in Functional Programming pages 124 140 Intellect UK The University of Chicago Press USA 2008 http ocamlgraph 1lri fr Lo c Correnson Pascal Cuoq Armand Puccetti and Julien Signoles Frama C User Manual December 2009 http frama c cea fr download user manual Beryllium 20090902 pdf Lo c Correnson Zaynah Dargaye and Anne Pacalet Frama C s WP plug in October 2011 http frama c com download frama c wp manual pdf Pascal Cuoq and Dam
8. 68 70 Mod 71 offset 68 Rneq 71 stmt 58 69 70 TCastE 71 typeinfo 69 70 varinfo 53 59 60 68 70 CilE 80 Cilutil 31 78 out_some 78 StmtHashtbl 59 78 StmtSet 59 Cmdline 32 65 66 80 Configuring 67 Early 66 Exit 67 Exiting 67 INDEX Extended 66 Extending 66 is_going_to_load 67 Loading 67 nop 67 run_after_configuring_ stage 67 run_after_early_stage 66 run_after_exiting_stage 67 run_after_extended_stage 66 run_after_extending_stage 57 60 61 run_after_loading_stage 67 run_after_setting_files 67 run_during_extending_stage 66 Command Line 25 ocode 51 Option 46 54 57 63 63 Parsing 65 Compilation see Makefile Computation see Internal State Computation 57 60 Ref 57 62 Config 80 Configuration see configure in configure in 17 18 36 81 check_plugin 19 37 check_plugin_dependencies 40 configure_library 37 configure_tools 37 DYNAMIC_plugin 37 ENABLE_plugin 37 FORCE_plugin 37 HAS_library 38 LIB_SUFFIX 38 OBJ_SUFFIX 38 plugin_require 39 plugin_require_external 38 plugin_use 39 plugin_use_external 38 REQUIRE_plugin 37 SELECTED_library 38 USE_plugin 37 Consistency 32 35 56 57 63 68 70 Context Switch 56 61 Control Flow Graph see CFG Copyright 23 76 CP 85 Dataflow 31 72 78 Dataflow analysis 31 78 Datatype 57 60 61 104 INDEX Copying 59 Mutable 58 Name 59 Persistent 58 Registration 58 Datatype 57 58 Bool 57
9. Example 5 22 Plug in from postpones its internal state in the following way File src kernel db mli module From struct val self Project Computation t ref end File src kernel db ml 60 5 11 PROJECT MANAGEMENT SYSTEM module From struct val self ref Project Computation dummy postponed end File src from register ml module Functionwise Dependencies Kernel function Make Table Function Froms Datatype struct let name functionwise_from let size 97 let dependencies Db Value self end let TOTS performed at module initialization runtime x Db From self Functionwise Dependencies self Plug in pdg uses from for computing its own internal state So it declares this dependency as follow File src pdg register ml module Tbl Kernel function Make Table PdgTypes Pdg Datatype struct let name Pdg State let dependencies postponed x let size 97 end let O Cmdline run after extended stage fun gt Project Computation add dependency Tbl self Db From self For standard plug ins it is possible to register state kinds in the same way that any other value through Dynamic register see Section 5 10 2 5 11 6 Direct Use of Low level Functor Project Computation Register Functor Project Computation Register is the only functor which really registers an internal state All the others internally use it In some cases e g if you define your own mutable record
10. If you wish the exact command line you have to set variable VERBOSEMAKE to yes like below make VERBOSEMAKE yes src kernel db cmo ocamlc opt c w Ael warn error A dtypes I src misc I src ai I src memory_state I src toplevel I src slicing_types I src pdg_types I src kernel I src logic I src cxx_types I src gui I lib plugins I lib I src lib I src project I src buckx I external I src project I src buckx I cil sre I cil src ext I cil srce fronte I cil src logic I cil ocamlutil g src kernel db ml In order to integrate a new plug in you have to extend section Plug ins For this purpose you have to include share Makefile plugin for each new plug in hence there are as many lines include share Makefile plugin as plug ins Makefile plugin is a generic makefile dedicated to plug in compilation Before its inclusion a plug in developer can set some vari ables in order to customize its behavior These variables are fully described in Section 6 3 3 These variables must not be used anywhere else in Makefile Moreover for setting them you must use and not In addition the results of the configure script must be exported in share Makefile config in see section 6 3 2 You must in particular add a line of the form Using only sets the variable value from the affectation point as usual in most programming languages whereas using would redefine the variable value for each of its occurrences in the m
11. see Section 2 2 5 and eventually specific test suites see Section 2 2 6 2 2 3 Hello Frama C World This section explains how to write the core of a kernel integrated Hello plug in This is a plug in which pretty prints Hello World whenever the option hello is set on the Frama C command line First we add a new subdirectory hello in directory src mkdir src hello This new directory is going to contain the source file of our new plug in If you want you can have a quick look at src which contains the kernel and existing plug ins We only use a few files from this directory in this tutorial We can now edit the source file of hello called src hello register ml It should contain exactly the same code than the file hello_world ml given page 15 in Section 2 1 2 in this regard there is no big difference between kernel integrated plug ins and the other ones 3As the plug in hello is tiny it has only one source file 17 CHAPTER 2 TUTORIAL Plug in tests suite Plug in directory Caption A part not covered in this tutorial registration points through hooks gt insertion points directly into the pointed file Figure 2 2 Kernel integrated Plug in Integration Overview 18 2 2 KERNEL INTEGRATED PLUG IN Recommendation 2 1 In Frama C the name of the main file of a plug in p should always be called either register ml or p_register ml At
12. Couple 59 Int 58 List 58 Nop 59 Ref 62 Db 17 20 30 32 52 52 53 60 74 79 80 From self 61 From self 60 Impact compute_pragmas 52 Main 14 17 extend 14 15 46 67 Main extend 65 progress 73 Value compute 55 59 is_computed 55 57 self 59 61 63 Db Properties 72 Db_types 52 80 Design 14 17 main_window_extension_points 73 register_extension 73 DISTRIB_FILES 42 doc 78 Documentation 16 20 73 78 86 Kernel 74 Plug in see Plug in Documentation Source 74 Tags 74 Dynamic 14 17 32 53 80 get 53 54 register 15 53 53 54 61 Emacs tags see Tags Entry Point 57 Entry point 14 Equality Physical 61 62 Structural 62 except 62 external 78 Extlib 31 79 mk_fun 20 NotYetImplemented 20 the 71 File 80 create_project_from_visitor 71 init_from_c_files 68 init_from_cmdline 68 init_project_from_cil_file 55 68 init_project_from_visitor 55 68 ForceCallDeps 65 FRAMAC_LIBDIR 15 42 FRAMAC_SHARE 15 42 From 60 61 Function 31 Globals 31 80 Annotations 72 set_entry_point 57 GUI 14 17 73 81 gui 81 Gui_init 80 Hash consing 58 Hashtable 57 58 60 78 Header 23 76 86 headers 76 78 Hello 18 35 Highlighting 73 Hook 14 17 index html 74 index prehtml 75 Initialization 20 53 57 60 65 66 install doc code 75 Internal State Cleaning 62 Internal Kind see State Kind Internal State 55 56 61 62 63 67 68
13. Intelligence amp Perception Edinburgh 1967 Donald Michie Memo functions and machine learning Nature 218 19 22 1968 George C Necula Scott McPeak Shree Prakash Rahul and Westley Weimer CIL Intermediate Language and Tools for Analysis and Transformation of C Programs In CC 02 Proceedings of the 11th International Conference on Compiler Construction pages 213 228 London UK 2002 Springer Verlag Julien Signoles Foncteurs imp ratifs et compos s la notion de projet dans Frama C In Hermann editor JFLA 09 Actes des vingti mes Journ es Francophones des Langages Applicatifs volume 7 2 of Studia Informatica Universalis pages 245 280 2009 In French Julien Signoles An OCaml Library for Dynamic Typing In Trends in Functional Pro gramming 2011 Submitted for publication Julien Signoles Une biblioth que de typage dynamique en OCaml In Hermann editor JFLA 11 Actes des vingt deuxi mes Journ es Francophones des Langages Applicatifs Studia Informatica Universalis pages 209 242 January 2011 In French 100 LIST OF FIGURES List of Figures 2 1 Plug in Integration Overview 14 2 2 Kernel integrated Plug in Integration Overview 18 4l Architecture Design 4 oscara addi ana Sea ea DAES 30 4 2 Differences between standard plug ins and kernel integrated ones 32 5 1 Representation of the Frama C Internal State 55 52 Indice
14. Lithium 20081201 e Changes fully new appendix e Command Line Options new sub section Storing New Dynamic Option Values e Configure in compliant with new implementations of configure_library and configure_tool e Exporting Datatypes now embeded in new section Plug in Registration and Access e GUI update in particular the full example has been removed e Introduction improved e Plug in Registration and Access fully new section e Project compliant with the new interface e Reference Manual integration of dynamic plug ins e Software architecture integration of dynamic plug ins e Tutorial improve part about dynamic plug ins e Tutorial use Db Main extend to register an entry point of a plug in e Website better highlighting of the directory containing the html pages Lithium 20081002 betal e GUI fully updated e Testing new sub section Alternative testing e Testing new directive STDOPT e Tutorial new section Dynamic plug ins e Visitor ChangeToPost in sub section Action Performed Helium 20080701 e GUI fully updated e Makefile additional variables of Makefile plugin e Project new important note about registration of internal states in Sub section Inter nal State Principle e Testing more precise documentation in the reference manual 97 APPENDIX A CHANGES Hydrogen 20080502 e Documentation new sub section Website e Documentation new ocamldoc tag plugin developer guide
15. Makefile Not written yet please report as feature request on http bts frama c com if you really need this section 3 7 Writing a Configure Script Not written yet please report as feature request on http bts frama c com if you really need this section 3 8 Testing your Plug in Not written yet please report as feature request on http bts frama c com if you really need this section 3 9 Getting your Plug in Usable by Others Not written yet please report as feature request on http bts frama c com if you really need this section 3 10 Writing your Plug in into the Journal Not written yet please report as feature request on http bts frama c com if you really need this section 3 11 Visiting the AST Not written yet please report as feature request on http bts frama c com if you really need this section 3 12 Getting your plug in Usable in a Multi Projects Setting Not written yet please report as feature request on http bts frama c com if you really need this section 3 13 Extending the Frama C GUI Not written yet please report as feature request on http bts frama c com if you really need this section 26 3 14 DOCUMENTING YOUR SOURCE CODE 3 14 Documenting your Source Code Not written yet please report as feature request on http bts frama c com if you really need this section 27
16. apply functor Project Datatype Imperative because a kernel function is composed of Cil_types fundec But it is still easy to perform the registration thanks to predefined functors Cil_ datatype VarinfoHashtbl Datatype List Kernel function Datatype Direct use of the low level functor In some cases e g registering a new variant type composed of a kernel function applying functor Project Datatype Register is required As input one has to provide e The type itself Hash consing is a programming technique saving memory blocks and speeds up operations on datastruc tures when sharing is maximal 10 13 3 7 58 5 11 PROJECT MANAGEMENT SYSTEM e How to copy it usually rebuild the structure by applying the right copy and copy functions on subterms e What is the representation of the type in memory and how to rebuild it while unmar shaling Pending further information define descr by let descr Project no_ descr e A name for the datatype Example 5 21 The type of postdominators is the following variant type postdominator Value of Cilutil StmtSet t Top The corresponding registered datatype used to store results of the postdominator computation is the following see file src postdominators compute ml Project Datatype Register struct type t postdominator let map f function Top Top Value set Value f set let copy map Cil datatype StmtSet copy let descr Project no desc
17. feature request on http bts frama c com if you really need this section 5 10 Plug in Registration and Access In this section we present how to register plug ins and how to access them Actually there are two different ways to register plug ins depending on whether they are kernel integrated or not cf Section 4 4 Section 5 10 1 indicates how to register and access a kernel integrated plug in while Sec tion 5 10 2 details how to register and access a standard plug in 51 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT 5 10 1 Kernel integrated Registration and Access Target readers kernel integrated plug in developers Prerequisite Accepting to modify the Frama C kernel Otherwise you can still register your plug in as any standard plug in see Section 5 10 2 for details A database called Db in directory src kernel groups together the API of all kernel integrated plug ins So it permits easy plug in collaborations Each kernel integrated plug in is only visible through Db For example if a plug in A wants to know the results of another plug in B it uses the part of Db corresponding to B A consequence of this design is that each plug in has to register in Db by setting a function pointer to the right value in order to be usable from others plug ins Example 5 11 Plug in Impact registers function compute_pragmas in the following way File src impact register ml let compute pragmas let O Db Impa
18. get O state let clear state Data default end As you can see the above implementation is error prone in particular it uses a double indi rection reference of reference So be happy that higher level functors like Computation Ref are provided which hide you such implementations 5 11 7 Selections Most operations working on a single project e g Project clear or Project on have two optional parameters only and except of type Project Selection t These parameters allow to specify which internal states the operation applies on As usual in OCaml stands for structural equality while resp stands for physical equality resp disequality 62 5 12 COMMAND LINE OPTIONS e If only is specified the operation is only applied on the selected internal states e If except is specified the operation is applied on all internal states except the selected ones e If both only and except are specified the operation only applied on the only internal states except the except ones A selection is roughly speaking a set of internal states Moreover it handles states dependencies that is the specificity of selections Example 5 24 The following statement clears all the results of the value analysis and all its dependencies in the current project Project clear only Project Selection singleton Db Value self Kind Select Dependencies O The argument Kind Select_Dependencies says that we also want to
19. macro are available through two variables which are substituted in the files generated by configure e HAS_library is set to yes or no depending on the availability of the library e SELECTED_library contains the name of the version selected as described above When checking for Objective Caml libraries and object files remember that they come in two flavors bytecode and native code which have distinct suffixes Therefore you should use the variables LIB_SUFFIX for libraries and OBJ_SUFFIX for object files to check the presence of a given file These variables are initialized at the beginning of the configure script depending on the availability of a native code compiler on the current installation Example 5 1 The library Lablgtksourceview used to have a better rendering of C sources in the GUI can be found either as part of Lablgtk2 or as an independent library This is checked through the following command configure_library GTKSOURCEVIEW OCAMLLIB lablgtk2 lablgtksourceview LIB SUFFIX OCAMLLIB lablgtksourceview lablgtksourceview LIB SUFFIX lablgtksourceview not found Moreover we want to distinguish the two cases as the independent library denotes a legacy version of Lablgtksourceview which has been merged with Lablgtk2 This is done by pattern matching on the variable SELECTED_GTKSOURCEVIEW as shown below case SELECTED GTKSOURCEVIEW in OCAMLLIB lablgtksourceview lablgtksourceview LIB SUFFIX HAS_LEGACY
20. own configuration file and can rely on the macros defined for Frama C In addition as mentioned in section 5 4 3 those plug ins can be compiled directly from Frama C s own Makefile In order for them to integrate well in this setting they should follow a particular layout described below First they need to be able to refer to the auxiliary configure ac file defining Frama C specific macros when they are used as stand alone plugins This can be done by the following code m4_define plugin_file Makefile m4_define FRAMAC_SHARE_ENV m4_normalize m4_esyscmd echo FRAMAC_SHARE m4_define FRAMAC_SHARE m4_ifval FRAMAC_SHARE_ENV FRAMAC_SHARE_ENV m4_esyscmd frama c print path m4_ifndef FRAMAC_M4_MACROS m4_include FRAMAC_SHARE configure ac plugin_file is the file which must be present to ensure that autoconf is called in the appro priate directory see documentation for the AC_INIT macro of autoconf configure ac can be found in two ways either by relying on the FRAMAC_SHARE shell variable when Frama C is not installed i e when configuring the plugin together with the main Frama C or by calling an installed Frama C when installing the plugin separately The inclusion of configure ac needs to be guarded to prevent multiple inclusions as the configuration file of the plugin might itself be included by configure in see section 5 4 3 for more details The configuration of the plugin itself can th
21. p to configure for a plug in p These options respectively forces p to be available and disables p its status is automatically not available Indeed configure in is organised in different sections specialized in different configuration checks Each of them begins with a title delimited by comments and it is highlighted when configure is executed These sections are described in Section 6 2 Now we focus on the modifications to perform in order to integrate a new plug in in Frama C 36 5 2 CONFIGURE IN 5 2 2 Addition of a Simple Plug in In order to add a new plug in you have to add a new subsection for the new plug in to Section Plugin wished This action is usually very easy to perform by copying pasting from another existing plug in e g occurrence and by replacing the plug in name here occurrence by the new plug in name in the pasted part In these sections plug ins are sorted according to a lexicographic ordering For instance Section Wished Plug in introduces a new sub section for the plug in occurrence in the following way occurrence check_plugin occurrence src occurrence support for occurrence analysis yes no The first argument is the plug in name the second one is the name of directory containing the source files of the plug in the third one is a help message for the enable occurrence option of configure the fourth one indicates if the plug in is enabled by default and the last one indicates if the pl
22. really need it Target readers It is only for e beginners who have to implement a plug in requiring very deep integration within the Frama C architecture e new Frama C kernel developers Prerequisite Getting the Frama C source This section will teach you how to write the most basic kernel integrated plug in and run it from the Frama C toplevel This plug in will be linked with the Frama C kernel and with all the other kernel integrated plug ins It is slightly more involved but allows a deeper integration within the Frama C architecture The running example in this section is the very same plug in Hello World than the one in the previous section 2 2 1 Setup Frama C uses a makefile which is generated by the script configure This script checks your system to determine the most appropriate Frama C configuration in particular the plug ins that should be made available This file is itself generated by the autotool autoconf Consequently you have to execute the following commands autoconf configure This generates a proper makefile and lists the available plug ins Now you are able to compile sources with make 16 2 2 KERNEL INTEGRATED PLUG IN make This compilation produces the following binaries in a standard configuration e bin toplevel byte and bin toplevel opt Frama C toplevel e bin viewer byte and bin viewer opt Frama C GUI e bin ptests byte Frama C testing tool Suffixes byte and op
23. results run tests and yes Behavior examine results examine Only examine current results do not no run tests show Run tests and show results but do no not examine them implies byte update Take current results as new oracles no do not run tests exclude suite Do not consider the given suite Misc diff cmd Use cmd to show differences between diff u results and oracles when examining results cmp cmd Use cmd to compare results against cmp s oracles when examining results use diff as cmp Use the same command for diff and no cmp jn Set level of parallelism to n 4 v Increase verbosity up to twice 0 help Display helps no Figure 6 11 ptests options run e g test of a feature that is currently developed and not fully operational yet If a test file is explicitly given on the command line of ptests it is always executed regardless of the presence of a DONTRUN directive As said in Section 5 5 2 these directives can be found in different places 1 default value of the directive as specified in Fig 6 12 2 inside file tests test_config 3 inside file tests subdir test_config for each sub directory subdir of tests or 4 inside each test file As presented in Section 5 5 3 alternative directives for test configuration lt special_ name gt can be found in slightly different places e default value of the directive as specified in Fig 6 12 e inside file tests test_config_ lt spec
24. tags for Frama C The tag since version should document any element intro duced after the very first release in order to easily know the required version of the Frama C kernel or specific plug ins In the same way the Frama C documentation generator provides a custom tag modify version description which should be used to document any element which semantics have changed since its introduction Furthemore the special tag plugin developer guide must be attached to each function used in this document Plug in APT A plug in should export no function itself the only visible plug in interface should be in Db Recommendation 5 5 To ensure this invariant the best way is to provide an empty inter face for the plug in The interface name of a plug in plugin must be Plugin mli Be careful to capitalization of the filename which is unusual in OCaml but required here for compilation purposes If you declare such an interface you also have to set the variable PLUGIN_HAS_MLI in your Makefile see Section 6 3 3 Internal Documentation for Kernel Integrated Plug ins The Frama C documen tation generator also produces an internal plug in documentation which may be use ful for the plug in developer itself This internal documentation is available via file doc code plugin index html for each plug in plugin You can add an introduction to this documentation into a file This file has to be assigned into variable PLUGIN_INTRO of the Makefile see Section
25. the annotations directly stored in the AST These states are the following e Globals Annotations which contains all the globals annotations e g global invari ants e Annotations which contains annotations associated with statements e g assertions e The field spec of kernel functions which contains annotations associated with functions e g preconditions e Properties_status should be used to get or to modify the status of annotations e Db Properties contains a number of operations over annotations 5 16 Locations Prerequisite Nothing special apart of core OCaml programming In Frama C different representations of C locations exist Section 5 16 1 presents them More over maps indexed by locations are also provided Section 5 16 2 introduces them 5 16 1 Representations There are four different representations of C locations Actually only three are really relevant All of them are defined in module Locations They are introduced below See the documen tation of src memory_state locations mli for details about the provided operations on these types e Type Location_Bytes t is used to represent values of C expressions like 2 or int amp a 13 With this representation there is no way to know the size of a value while it is still possible to join two values Roughly speaking it is represented by a mapping between C variables and offsets in bytes e Type location is used to represent the right part of a C
26. this document corresponds to the version Nitrogen 20111001 October 10 2011 of Frama C However the development of Frama C is still ongoing features described here may still evolve in the future Acknowledgements We gratefully thank all the people who contributed to this document Patrick Baudin Richard Bonichon Pascal Cuoq Pierre Lo c Garoche Philippe Herrmann Nikolai Kosmatov Benjamin Monate Yannick Moy Anne Pacalet Armand Puccetti Muriel Roger and Boris Yakobowski We also thank Johannes Kanig for his Mipost support the tool used for making figures of this document http frama c com http www rntl org projet resume2005 cat htm Shttp mlpost lri fr Chapter 1 Introduction Frama C Framework for Modular Analyses of C is a software platform which helps the development of static analysis tools for C programs thanks to a plug ins mechanism This guide aims at helping developers program within the Frama C platform in particular for developing a new analysis or a new source to source transformation through a new plug in For this purpose it provides a step by step tutorial a general presentation of the Frama C software architecture a set of Frama C specific programming rules and an overview of the API of the Frama C kernel However it does not provide a complete documentation of the Frama C API and in particular it does not describe the API of existing Frama C plug ins This API is documented in th
27. this point we have a compilable plug in made of a main function run 2 2 4 Configuration and Compilation Here we explain how to compile the hello plug in Section 5 2 and 5 3 provide more details about the configuration and compilation of plug ins Configuration As explained in Section 2 2 1 Frama C uses both autoconf and make in order to compile Consequently we have to modify both files configure in and Makefile in order to compile our plug in within Frama C In both files predefined scripts help with plug in integration In order to compile the hello plug in first add the following lines into configure in They indicate how to configure hello especially whether it has to be compiled or not File configure in Add the following lines after other plug in configurations in the section Plug in sections hello check_plugin hello src hello support for hello plug in yes no These lines correspond to the standard way of configuring a new plug in The function check_plugin is defined in configure in Its first argument is the plug in name the second one is the plug in directory the directory containing the plug in source files the third one is a help message the fourth one indicates whether the plug in is available by default here yes says that the plug in is available by default and a user may use option disable hello to deactivate the plug in and the last one indicates whether the plug in will be dynamically
28. type checker complains if the third argument here the value run has not the type unit unit Calling a previously registered function The signature of function Dynamic get is as follows val get plugin string gt string a Type t gt a The arguments must be the same than the ones used at value registration time with Dynamic register Otherwise depending on the case you will get a compile time or a runtime error Example 5 14 Here is how the previously registered function run of Hello may be applied let O Dynamic get plugin Hello run Type func Type string Type unit O The given strings and the given type value must be the same than the ones used when registering the function Otherwise an error occurs at runtime Furthermore the OCaml type checker will complain either if the third argument here is not of type unit or if the returned value here also is not of type unit 5 11 Project Management System This section is out of date Please report as feature request on http bts frama c com if you really need it Prerequisite knowledge of OCaml module system and labels In Frama C a key notion detailed in this section is the one of project An overview as well as technical details may also be found in a related article in French 18 Section 5 11 1 first introduces the general principle of project Then Section 5 11 2 explains how to simply use them Section 5 11 3 introduces the so called
29. with extreme caution as f could break some invariants of the kernel e ChangeDoChildrenPost v f the old node is replaced by v the visit goes on with the children of v and when it is finished f is applied to the result In the case of vstmt_aux f is called after the annotations in the annotations table have been visited but before they are attached to the new statement that is they will be added to the result of f Similarly vglob_aux will consider the result of f when filling the table of globals e JustCopyPost f is only meaningful for the copy visitor Performs a fresh copy of the nodes and all its children and applies f to the copy 5 14 4 Visitors and Projects Visitors take an additional argument which is the project in which the transformed AST should be put in Note that an in place visitor see next section should operate on the current project otherwise two projects would share the same AST If this is not the case it is up to the developer to ensure that the copy is done by other means so that there is no sharing Note that the tables of the new project are not filled immediately Instead actions are queued and performed when a whole Cil_types file has been visited One can access the queue with the get_filling_actions method and perform the associated actions on the new project with the fi11_global_tables method 5 14 5 In place and Copy Visitors The visitors take as argument a visitor_behavior which comes in
30. 5 53 t 53 54 unit 15 53 Type value 53 79 Typing 30 31 UNPACKED_DIRS 41 52 85 Value 41 Variable Global 31 VERBOSEMAKE 0 85 Visitor 26 67 Behavior 69 70 Cil see Cil Visitor Copy 55 69 70 In Place 69 69 Visitor 31 80 generic_frama_c_visitor 67 71 vglob_aux 68 vstmt_aux 68 Website 75 109
31. 6 3 3 In order to ease access to this internal documentation you have to manually edit the file doc index html in order to add an entry for your plug in in the plug in list 74 5 19 LICENSE POLICY Internal Documentation for External Plug ins External plug ins can be documented in the same way as plug ins that are compiled together with Frama C However in order to be able to compile the documentation with make doc you must have generated the documentation of Frama C s kernel make doc see above and installed it with the make install doc code command 5 18 3 Website Target readers developers with a SVN access The html sources of the Frama C website belong to directory doc www src Each plug in available through the Frama C website http frama c com may have its own webpage For each plug in p the source of its webpage should be called p prehtml this file is pre processed by the makefile generating the whole website The format of this page looks like below lt head gt lt hi gt Impact plug in lt h1 gt Plug in description lt foot gt This page should be referenced from the page http www frama c cea fr plugins html For this purpose you have to edit files plugins prehtml and index prehtml In order to generate the html pages from directory doc www src just execute make html_pages The generated website is available in directory doc www export and the homepage is doc www export ind
32. 66 80 C Intermediate Language see Cil Call graph computation 31 Callgraph 31 78 CEA_INRIA_LGPL 76 CEA_LGPL 23 CFG 80 Cfg 78 check_plugin 18 37 CIL 78 103 Index Syntactic Analysis 78 Visitor 80 Cil 29 30 31 35 67 API 30 31 AST see AST Visitor 67 Entry Point 68 Cil 31 78 ChangeDoChildrenPost 69 70 ChangeTo 68 70 ChangeToPost 69 cilVisitor 67 68 copy_visit 69 71 DoChildren 68 71 fill_global_tables 69 get_name 69 get_filling_actions 69 71 get_original_name 69 inplace_visit 69 JustCopy 69 70 JustCopyPost 69 1zero 71 reset_behavior_name 69 set_name 69 SkipChildren 68 70 type0f 71 vexpr 71 vglob 68 visitAction 68 visitCilAstT ype 68 visitCilFile 68 visitCilFileCopy 68 visitCilFileSameGlobals 68 visitor_behavior 69 vlogic_ctor_info_decl 68 vlogic_ctor_info_use 68 vlogic_info_decl 68 vlogic_info_use 68 vlogic_type_info_decl 68 vlogic_type_info_use 68 vlogic_var_decl 68 vlogic_var_use 68 voffs 68 vstmt 68 vvdec 68 vvrbl 68 cil 35 78 78 ocamlutil 78 src 31 78 ext 78 frontc 79 logic 79 Cil_computation 57 60 StmtHashtbl 59 Cil_datatype 57 58 Stmt 58 StmtSet 59 Varinfo 59 VarinfoHashtbl 58 Cil_types 31 78 BinOp 71 compinfo 69 70 Ctype 71 Div 71 enuminfo 69 70 fieldinfo 69 70 file 67 70 fundec 58 global 68 logic_ctor_info 68 logic_info 68 70 logic_type_info 68 logic_var
33. All the GUI plug in extensions share the same window and same wid gets So conflicts can occur especially if you specify some attributes on a predefined object For example if a plug in wants to highlight a statement s in yellow and another one wants to highlight s in red at the same time the behavior is not specified but it could be quite difficult to understand for an user 5 18 Documentation Prerequisite knowledge of ocamldoc Here we present some hints on the way to document your plug in First Section 5 18 1 in troduces a quick general overview about the documentation process Next Section 5 18 2 focuses on the plug in source documentation Finally Section 5 18 3 explains how to modify the Frama C website 73 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT 5 18 1 General Overview Command make doc produces the whole Frama C source documentation in HTML format The generated index file is doc code html index html A more general purpose index is doc index html from which the previous index is accessible The previous command takes some times So command make html only generates the ker nel documentation i e Frama C without any plug in while make PLUGIN_NAME _DOC by substituting the right value for PLUGIN_NAME generates the documentation for a single plug in 5 18 2 Source Documentation Each plug in should be properly documented Frama C uses ocamldoc and so you can write any valid ocamldoc comments ocamldoc
34. Cleaning 63 Dependency 57 60 61 63 Postponed 60 66 Functionalities 56 Global Version 61 Kind 60 Local Version 61 62 Name 60 61 Registration 56 57 59 Selection see Selection Sharing 62 105 The Frama C One 55 63 Inthash 78 Ival 31 79 Journal 14 17 32 80 Journalization 26 51 66 67 Kernel 29 30 31 36 61 79 82 86 Toolbox 79 kernel 79 Kernel Function 58 Kernel functions 72 Kernel_function 59 80 Datatype 58 59 Make_Table 60 61 Kernel_type 53 80 Kind Only_Select_Dependencies 55 Select_Dependencies 63 Kui 80 Lablgtk 38 39 73 Lablgtksourceview 38 Lattice 30 31 73 79 Lattice 64 Lesser General Public License see LGPL Lexing 30 31 LGPL 23 76 lib 78 79 fc 78 gui 78 plugins 78 Library 36 78 Configuration 37 81 Dependency 38 licences 76 License 23 75 86 LICENSES 76 licenses 78 Linking 30 32 65 66 Lmap 31 73 79 Lmap_bitwise 31 73 79 Loading 54 55 57 67 Location 72 79 Locations 31 72 79 location 72 Location_Bits 72 Location_Bytes 72 valid_enumerate_bits 72 Zone 72 Log 32 80 INDEX abort 48 add_listener 49 debug 47 error 48 failure 48 fatal 48 feedback 47 log 49 log_channel 50 Messages 47 new_channel 50 print_delayed 51 print_on_output 51 result 47 set_echo 49 set_output 51 verify 48 warning 47 with_log 50 with_log_channel 50 Logging see Messages logic 79 Lo
35. ILE TREE e src frontc is the C frontend which converts C code to the corresponding Cil AST It should not be used by a Frama C plug in developer e src logic is the ACSL frontend which converts logic code to the corresponding Cil AST The only useful modules for a Frama C plug in developer are Logic_const which provides some predefined logic constructs terms predicates and Logic_typing which allows to dynamically extend the logic type system 6 1 2 The src directory The source files of Frama C are split into different sub directories inside src Each sub directory contains either a plug in implementation or some specific parts of the Frama C kernel Each plug in implementation can be split into two different sub directories one for ex ported type declarations and related implementations visible from Db see Chapter 4 and Section 5 10 1 and another for the implementation provided in Db Kernel directories are shown Figure 6 3 More details are provided below Kind Name Specification Reference kernel Kernel toolbox logic Logic toolbox FAR x Mea interpretation toolbox Section 5 16 memory_states Memory state toolbox Section 5 16 project Project library Section 5 11 Libraries lib Miscellaneous libraries misc Additional useful operations Entry points gui Graphical User Interface Section 5 17 Figure 6 3 Kernel directories e Directory kernel contains the kernel toolbox over Cil Main kernel
36. IN_CMO hello_world include FRAMAC_SHARE Makefile dynamic FRAMAC_SHARE must be set to the Frama C share directory while FRAMAC_LIBDIR must be set to the Frama C lib directory PLUGIN_NAME is the capitalized name of your plug in while PLUGIN_CMO is the list of the files cmo generated from your OCaml sources To run your specific Makefile you must have properly installed Frama C before You may possibly need to do make depend before running make Which variable can be set and how they are useful is explained Section 6 3 3 Furthermore Section 6 3 4 explains the specific features of Makefile dynamic 5 4 2 Calling a Plug in Specific Makefile from the Frama C Makefile Target readers kernel integrated plug in developers using the SVN repository of Frama C Even if you are writing a kernel integrated plug in it is useful to have your plug in specific Makefile For instance it allows you to easily release your plug in independently of Frama C However if your version of Frama C is changing frequently it is useful to compile together Frama C and your plug in without installing Frama C each time To reach this goal you have to mix the integration in Makefile described in Section 5 3 and the solution presented in this section in the section Plug ins of Makefile you just have to set few variables before including your plug in specific Makefile Example 5 5 For compiling the plug in Ltl_to_acsl the following lines are added into
37. Makefile PLUGIN_ENABLE ENABLE_LTL_TO_ACSL PLUGIN_DIR src ltl_to_acs1l PLUGIN_DYNAMIC ODYNAMIC_LTL_TO_ACSLQ DISTRIB_FILES PLUGIN_DIR Makefile include PLUGIN_DIR Makefile 5 4 3 Compiling Frama C and external plug ins at the same time Target readers plug in developers using the SVN repository of Frama C It is also possible to have a completely independent plug in recompile and test together with Frama C s kernel For that Frama C must be aware of the existence of the plug in This can be done in two ways 42 5 5 TESTING e All sub directories of src directory in Frama C sources which are not known to Frama C s kernel are assumed to be external plug ins e One can use the enable external option of configure which takes as argument the path to the plugin In the first case the plug in behaves as any other built ins plugins autoconf run in Frama C s main directory will take care of it and it can be enabled or disabled in the same way as the others If the plug in has its own configure in or configure ac file the configuration instructions contained in it in particular additional dependencies will be read as well In the second case the plugin is added to the list of external plugins at configure time If the plugin has its own configure it is run as well 5 5 Testing In this section we present ptests a tool provided by Frama C in order to perform non regression and unit tests ptests runs t
38. OPT directive takes as default set of options the last OPT directive s of the preceding configuration level If the preceding configuration level contains several OPT directives hence several test cases STDOPT is applied to each of them leading to the same number of test cases The syntax for this directive is the following STDOPT opt options are always given between quotes An option following a is added to the current set of options while an option following a is removed from it The directive can be empty meaning that the corresponding test will use the standard set of options As with OPT each STDOPT corresponds to a different set of test case s e The syntax for directive EXECNOW is the following EXECNOW LOG file BIN file cmd Files after LOG are log files generated by command cmd and compared from oracles whereas files after BIN are binary files also generated by cmd but not compared from 93 CHAPTER 6 REFERENCE MANUAL oracles Full access path to these files have to be specified only in cmd All the commands described by directives EXECNOW are executed in order and before running any of the other directives If the execution of one EXECNOW directive fails 4e has a non zero return code the remaining actions are not executed EXECNOW directives from a given level are added to the directives of the following levels e The FILEREG directive contains a regular expression indicating w
39. S ee DURE Ba DE a af Writing a Configure SONP se o cachea saira PREP e ee Se eS 3 0 lesng your PIG 22 45 484466444 2 oy ee he BR ae eee eG CONTENTS 3 9 Getting your Plug in Usable by Others 26 3 10 Writing your Plug in into the Journal 26 LL Vetma the AST 2 di bee kA neue tisane CES e 26 3 12 Getting your plug in Usable in a Multi Projects Setting 26 3 13 Extending the Frama C GUI ov a 44 ausa Bee Re a 26 3 14 Docume nting your Source Code s aa soca Ped ee Ge eevee e 4 27 Software Architecture 29 4 1 General Description p ea 422844 da de 40445 REE eae ee Rae 29 42 Cil C Intermediate Language Lau bee eee eee ee 31 dd WG LL a Re EER eee ded eee Re IRIS TAN EN 31 Ad PIERRE ui ine id ee La NN a a he oh ee ee 32 Advanced Plug in Development 35 5 1 File Tr Overview 44 be carena bye ma 4 amp au pe de 35 02 CODEN sa eee WED Ne di be ee oe 2 36 Dal Pee Laser tie Ladies OR ee eRe SE ORS 36 5 2 2 Addition of a Simple Plug in 6 24446 4444484442 sew ss 37 5 2 3 Configuration of New Libraries or Tools 37 5 2 4 Addition of Library Tool Dependencies 38 5 2 5 Addition of Plug in Dependencies 39 5 20 External plugins o escada 4 seria ee Ee 39 Do WWII s a LD gp ank a DU St AMENER SR ER MU A o 40 5 4 Plug in Specific Makefile 41 9 4 1 Using M
40. Software Analyzers Developer Manual cen List Plug in Development Guide Release Nitrogen 20111001 Julien Signoles with Loic Correnson and Virgile Prevosto CEA LIST Software Reliability Laboratory Saclay F 91191 2009 CEA LIST This work has been supported by the CAT ANR project ANR 05 RNTL 00301 Contents Very Important Preliminary Warning 8 Foreword 9 1 Introduction 11 1 1 About this document esa oe d ad e de beau set eme ED 11 DA UPME ce un sa Ua SAR DEE Rs a DEE ORAS EH BD 12 2 Tutorial 13 2 Shen PER e se dau ie lan sa dames dd selon pe 13 2 1 1 Plug in Integration Overview 13 fie Hello Frama C World sa ss oe a Bie ERG ie be mA SE a an 14 2 2 Kernel integrated Plug in 16 A 16 2 2 2 Plug in Integration Overview 17 22 0 Helle Frama C World 4 45 ga bk eee kee eRe ve Ee 17 2 2 4 Configuration and Compilation 19 2 2 5 Connection with the Frama C World 20 Pa CESE LA a we la oe a A ew Ba g 22 22 Copyright your Work i re be bae aa Oe p a ee eS 23 3 Tutorial of the Future 25 3 1 What a Plug in Look Like 25 32 A Surple SOPE e uke koh ge enh eR ek ae min de DUR do node ne 25 3 3 Registering a Script as a Plug in 34 Displaying Messages users Ye ae ae a a ee 3 5 Adding Command Line Options 3 0 Writings Makenle scq ou ore du aa de e
41. _CMO 41 53 85 88 plugin_TYPES_CMO 91 plugin_TYPES_CMX 91 PLUGIN_Types_TODOC 90 PLUGIN_UNDOC 41 88 plugins prehtml 75 Postdominator 59 Preprocessing 31 Print 64 PRINT_CP 85 Printer 80 Project 26 35 54 63 67 69 79 Current 55 56 61 63 69 Initial 68 Use 55 Project 14 17 30 32 55 clear 55 62 63 Computation add_dependency 61 dummy 60 Register 57 60 61 62 copy 98 current 55 55 Datatype Imperative 58 58 Persistent 58 58 Register 57 98 59 I0Error 55 load 55 no_descr 59 on 56 62 63 INDEX save 55 Selection 62 singleton 55 63 set_current 55 55 56 t 55 project 79 Properties_status 72 Ptests 22 43 86 91 Rangemap 31 Register 18 Saving 35 54 55 57 99 Selection 57 62 self 60 60 Session 55 share 78 Sharing 69 70 Widget 73 Side Effect 62 65 Slicing 76 Sparecode 43 Special_hooks 80 src 35 78 79 ai 31 kernel 31 lib 31 memory_state 31 misc 31 project 32 State Kind 60 Stmts_graph 80 SVN 22 Tags 16 86 Test 16 21 26 43 86 91 Configuration 44 Directive 44 Header 44 45 Suite 18 43 44 78 Test Directive CMD 93 COMMENT 93 DONTRUN 93 EXECNOW 93 FILEREG 93 94 FILTER 93 GCC 93 OPT 21 44 93 STDOPT 93 108 INDEX test_config 44 92 94 tests 43 78 91 Tool 36 Configuration 37 81 Dependency 38 Type First class value 51 Type 14 17 32 53 79 AlreadyExists 53 func 1
42. _GTKSOURCEVIEW yes esac 5 2 4 Addition of Library Tool Dependencies Dependencies upon external tools and libraries are governed by two macros e plugin_require_external plugin library indicates that plugin requires library in order to be compiled e plugin_use_external plugin library indicates that plugin uses library but can nev ertheless be compiled if library is not installed potentially offering reduced functional ity Recommendation 5 1 The best place to perform such extensions is just after the addition of p which sets the value of ENABLE_p 38 5 2 CONFIGURE IN Example 5 2 Plug in gui requires Lablgtk2 12 So just after its declaration there are the following lines in configure in plugin_require_external gui lablgtk This line specify that Lablgtk2 must be available on the system if the user wants to compile gut 5 2 5 Addition of Plug in Dependencies Adding a dependency with another plug in is quite the same as adding a dependency with an external library or tool see Section 5 2 4 For this purpose configure in uses two macros e plugin_require pluginl plugin2 states that pluginl needs plugin2 e plugin_use pluginl plugin2 states that pluginl can be used in absence of plugin2 but requires plugin2 for full functionality There can be mutual dependencies between plugins This is for instance the case for plugins value and from 5 2 6 External plugins External plug ins can have their
43. able PLUGIN_CMO do not write their file path nor their file extension e Variables of the form PLUGIN_ _FLAGS are plug in specific flags for ocamlc ocamlopt ocamldep or ocamldoc e Variable PLUGIN_GENERATED is files which must be generated before computing plug in dependencies In particular this is where ml files generated by ocamlyacc and ocamllex must be placed if needed e Variable PLUGIN_DEPENDS is the other plug ins which must be compiled before the con sidered plug in Note that in a normal context it should not be used because a plug in interface should be empty see Chapter 4 e Variable PLUGIN_UNDOC is the source files for which no documentation is provided Do not write their file path which is automatically set to PLUGIN_DIR 88 6 3 MAKEFILES Kind Name Specification PLUGIN_DEPFLAGS Plug in specific flags for ocamldep Dependencies PLUGIN_GENERATED Plug in files to compiled before running ocamldep PLUGIN_DEPENDS Other plug ins to compiled before no the considered one PLUGIN_DOCFLAGS Plug in specific flags for ocamldoc PLUGIN_UNDOC Source files with no provided doc Documentation umentation PLUGIN_TYPES_TODOC Additional source files to docu ment PLUGIN_INTRO Text file to append to the plug in introduction PLUGIN_HAS_EXT_DOC Whether the plug in has an exter nal pdf manual PLUGIN_NO_TESTS Whether there is no plug in spe cific test directory Testing PLUGIN_TESTS_DIRS tests to be include
44. affectation including bitfields It is represented by a Location_Bits t see below attached to a size It is possible to join two locations if and only if they have the same sizes e Type Location_Bits t is similar to location_Byte t with offsets in bits instead of bytes Actually it should only be used inside a location e Type Zone t is a set of bits without any specific order It is possible to join two zones even if they have different sizes Recommendation 5 4 Roughly speaking locations and zones have the same purpose You should use locations as soon as you have no need to join locations of different sizes If you require to convert locations to zones use the function Locations valid_enumerate_bits As join operators are provided for these types they can be easily used in abstract interpre tation analyses which can themselves be implemented thanks to one of functors of module Dataflow see Section 6 1 1 72 5 17 GUI EXTENSION 5 16 2 Map Indexed by Locations Modules Lmap and Lmap_bitwise provide functors implementing maps indexed by locations and zones respectively The argument of these functors have to implement values attached to indices locations or zones These implementations are quite more complex than simple maps because they automati cally handle overlaps of locations or zones So such implementations actually require that structures implementing values attached to indices are lattices i e implement
45. akefile see Section 6 2 The Two Flavors of Variables of the GNU Make Manual 11 40 5 4 PLUG IN SPECIFIC MAKEFILE ENABLE_plugin ENABLE_plugin so that make will know whether the plugin is supposed to compiled or not Other variables may be exported there as well DYNAMIC_plugin HAS_library if the corresponding information is needed during compilation Example 5 3 For compiling the plug in Value the following lines are added into Makefile HEEL LL TAITTITITITITITITITITITITITITITITITIT Value analysis Y TUTTT TTA TTT TT ATT aT EEE EEE EEE EEE PLUGIN_ENABLE ENABLE_VALUE_ANALYSIS PLUGIN_NAME Value PLUGIN_DIR src value PLUGIN_CMO state_set kf_state eval kinstr register PLUGIN_GUI_CMO value_gui PLUGIN_HAS_MLI yes PLUGIN_NO_TEST yes PLUGIN_UNDOC value_gui ml include Makefile plugin As said above you cannot use the parameters of Makefile plugin anywhere in Makefile You can yet use some plugin in specific variables once Makefile plugin has been included These variables are detailed in Section 6 3 3 One other variable has to be modified by a plug in developer if he uses files which do not belong to the plug in directory that is if variable PLUGIN_TYPES_CMO is set This variable is UNPACKED_DIRS and corresponds to the list of non plug in directories containing source files A plug in developer should not have to modify any other part of Makefile Makefile config in or Makefile plugin
46. akefile dynamic 41 5 42 Calling a Plug in Specific Makefile from the Frama C Makefile 42 5 4 3 Compiling Frama C and external plug ins at the same time 42 o A Ra M REVERS AMAR e RES 43 540 1 USME PRESS 4 Lu a e Las tabs al sue a ef a 43 210 2 COMMBUPAION LME UNE A Rs LS 44 DoS Alternative TESTA 44 4 6G amp 4 GS Ow de EN ERE AAA 45 5 6 Plug in General Services 45 Ot Logging Services o du na ne s a d un a be date Ee Eee aa dia 46 Olek From printi tO LOE ace au eus dur spas der pra te 47 5 7 2 Log Quick Reference 47 Dio Logging Routine Options 4 44 sasada de be ee an 48 5 7 4 Advanced Logging Services 49 9 8 Types as first class VAMOS a s cc 4 da pas a Robe au ge 8 mu ab 4 51 5 9 5 10 5 11 5 12 5 13 5 14 5 15 5 16 0 17 5 18 D19 Reference Manual DL 6 2 CONTENTS IQUEMANDZM O 4 ke a has A op dde 51 Plug in Registration and Access 51 5 10 1 Kernel integrated Registration and Access 52 5 10 2 Dynamic Registration and Access 53 Project Management System 54 5 11 1 Overview and Key Notions 54 Sll Using Projects aces eo a unes da Mee Eee wee Alay 55 5 11 3 Internal State Principle o 56 5 11 4 Registe
47. alue 53 Vp1 p2 of type tsuch that p1 p2 set pi get p2 5 4 Invariant 5 1 ensures that there is no sharing with any fresh value of a same internal state so each new project has got its own fresh internal state Invariant 5 2 ensures that cleaning a state resets it to its initial value Invariant 5 3 ensures that there is no sharing with any copy Invariant 5 4 is a local independence criteria which ensures that modifying a local version does not affect any other version different of the global current one by side effect Example 5 23 To illustrate this we show how functor Computation Ref registering a state corresponding to a reference is implemented module Ref Data REF INPUT Info Signature NAME DPDS struct type data Data t let create ref Data default let state ref create Here we use an additional reference our local version is a reference on the right state We can use it in order to safely and easily implement get and set required by the registration include Project Computation Register Datatype Ref Data struct type t data ref we register a reference on the given type let create create let clear tbl tbl Data default let get state let set x state x let clear _if project _ _ false end Info For users of this module we export standard operations which hide the local indirection required by the project management system let set v state v let
48. an be replaced by another one Typically it would be loaded from disk through the load option or computed by running a journal see Section 5 9 As like as for the other stages a first the command line options registered for the Cmdline Loading stage are treated b then the hooks registered through Cmdline run_after_loading_stage are ex ecuted in an unspecified order These functions actually change the initial state of Frama C with the specified one The Frama C kernel verifies as far as possible that only one new initial state has been specified Normally plug ins should never register hooks for this stage unless they actually set a different initial states than the default one In such a case They must call the function Cmdline is_going_to_load while initializing 4 The Configuring Stage this is the usual place for plug ins to perform special initialization routines if necessary before having their main entry points executed As for previous stages a first the command line options registered for the Cmdline Configuring stage are treated Command line parameters that do not begin by an hyphen character are not options and are treated as C files Thus they are added to the list of files to be preprocessed or parsed for building the AST on demand b then the hooks registered through Cmdline run_after_configuring_stage are executed in an unspecified order 5 The Setting Files Stage this stage sets the C files to
49. analyze according to those indicated on the command line More precisely a first each argument of the command line which does not begin by an hyphen character is registered for later analysis b then the hooks registered through Cmdline run_after_setting_files are exe cuted in an unspecified order 6 The Main Stage this is the step where plug ins actually run their main entry points registered through Db Main extend For all intents and purposes you should consider that this stage is the one where these hooks are executed 5 14 Visitors Prerequisite knowledge of OCaml object programming Cil offers a visitor Cil cilVisitor that allows to traverse parts of an AST It is a class with one method per type of the AST whose default behavior is simply to call the method corresponding to its children This is a convenient way to perform local transformations over a whole Cil_types file by inheriting from it and redefining a few methods However the original Cil visitor is of course not aware of the internal state of Frama C itself Hence there exists another visitor Visitor generic_frama_c_visitor which handles projects in 67 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT a transparent way for the user There are very few cases where the plain Cil visitor should be used Basically as soon as the initial project has been built from the C source files i e one of the functions File init_ has been applied only
50. ation and Access updateed according to API changes Documentation updated and improved Introduction is aware of the Frama C user manual Logical Annotations fully new section Tutorial fix an efficiency issue with the Makefile of the Hello plug in Beryllium 20090902 Makefiles update according to the new Makefile kernel Beryllium 20090901 Makefiles update according to the new makefiles hierarchy Writing messages fully documented Initialization Steps the different stages are more precisely defined The implemen tation has been modified to take into account specifities of dynamically linked plug ins Project Management System mention value descr in Datatype Makefile plugin add documentation for additional parameters Beryllium 20090601 betal Initialization Steps update according to the new implementation Command Line Options update according to the new implementation Plug in General Services fully new section introducing the new module Plugin File Tree update according to changes in the kernel Makefiles update according to the new file Makefile dynamic and the new file Makefile config in Architecture update according to the recent implementation changes Tutorial update according to API changes and the new way of writting plug ins 96 e configure in update according to changes in the way of adding a simple plug in e Plug in Registration and Access update according to the new API of module Type
51. clear all the states which depend on the value analysis Use selections carefully if you apply a function f on a selection s and if f handles a state which does not belong to s then the Frama C state becomes lost and inconsistent Example 5 25 The following statement applies a function f in the project p which is not the current one For efficiency purpose we restrict the considered states to the command line options see Section 5 12 Project on only Plugin get_selection O pf O This statement only works if f gets only values of the command line options If it tries to get the value of another state the result is unspecified and all actions using any state of the current project and of project p also become unspecified 5 12 Command Line Options This section is out of date Please report as feature request on http bts frama c com if you really need it Prerequisite knowledge of the OCaml module system Values associated with command line options are called parameters The parameters of the Frama C kernel are stored in module Parameters while the plug in specific ones have to be defined in the plug in source code In Frama C a parameter is actually a structure implementing signature Plugin Parameter in order to handle projects each parameter is indeed an internal state see Section 5 11 5 Actually a bunch of signatures extended Plugin Parameter are provided in order to deal with the usual parameter types For e
52. ct compute pragmas compute pragmas So each developer who wants to use this function calls it by pointer dereferencing like this let O Db Impact compute pragmas If a kernel integrated plug in has to export some datatypes usable by other plug ins such datatypes have to be visible from module Db Thus they cannot be declared in the plug in implementation itself like any other plug in declaration because postponed type declarations are not possible in Objective Caml Such datatypes are called plug in types The solution is to put these plug ins types in some files linked before Db hence you have to put them in another directory than the plug in directory The best way is to create a directory dedicated to types even if it is possible to put a single file in another directory or to put a single type in an existing file like src kerne1 db_types mli Recommendation 5 2 The suggested name for this directory is p_ types for a plug in p If you add such a directory you also have to modify Makefile by extending variable UNPACKED_DIRS see Section 6 3 3 Example 5 12 Suppose you are writing a plug in plug in which exports a specific type t corresponding to the result of the plug in analysis The standard way to proceed is the following File src plugin_ types plugin_ types mli typar File src kernel db mli module Plugin sig val run and get unit Plugin_types t ref Run plugin analysis if it was never launched befo
53. d in the default test suite PLUGIN_TESTS_DIRS_DEFAULT Directories containing tests PLUGIN_TESTS_LIBS Specific cmo files used by plug in tests PLUGIN_NO_DEFAULT_TEST Whether to include tests in default test suite PLUGIN_INTERNAL_TEST Whether the test suite of the plug in is located in Frama C s own tests directory PLUGIN_DISTRIBUTED_BIN Whether to include the plug in in no Distribution binary distribution PLUGIN_DISTRIBUTED Whether to include the plug in in no source distribution PLUGIN_DISTRIB_EXTERNAL Additional files to be included in no the distribution Figure 6 9 Special parameters of Makefile dynamic and Makefile plugin 89 CHAPTER 6 REFERENCE MANUAL Variable PLUGIN_TYPES_TODOC is the additional source files to document with the plug in They usually belong to src plugin_types where plugin is the plug in name see Section 5 10 1 e Variable PLUGIN_INTRO is the text file to append to the plug in documentation intro duction Usually this file is doc code intro_plugin txt for a plug in plugin It can contain any text understood by ocamldoc e Variable PLUGIN_HAS_EXT_DOC is set to yes if the plug in has its own reference manual It is supposed to be a pdf file generated by make in directory doc PLUGIN_NAME e Variable PLUGIN_NO_TEST must be set to yes if there is no specific test directory for the plug in e Variable PLUGIN_TESTS_DIRS is the directories containing plug in tests Its defa
54. e are several sections corresponding to plug ins see Section 6 3 3 This is the part that a plug in developer has to modify in order to add compilation directives for its plug in Generic variables provides variables containing files to be linked in different contexts Toplevel provides rules for building the files of the form bin toplevel GUI provides rules for building the files of the form bin viewer Standalone obfuscator provides rules for building the Frama C obfuscator Tests provides rules to execute tests see Section 5 5 Emacs tags provides rules which generate emacs tags useful for a quick search of OCaml definitions Documentation provides rules generating Frama C source documentation see Sec tion 5 18 Installation provides rules for installing different parts of Frama C File headers license policy provides variables and rules to manage the Frama C license policy see Section 5 19 Makefile rebuilding provides rules in order to automatically rebuild Makefile and configure when required Cleaning provides rules in order to remove files generated by makefile rules Depend provides rules which compute Frama C source dependencies Ptests provides rules in order to build ptests see Section 5 5 Source distribution provides rules usable for distributing Frama C 86 6 3 MAKEFILES Kind Name Specification PLUGIN_NAME Module name of the plug in Usual PLUGIN_DIR a containing plug in so
55. e chapter to another one Pointers to reference manuals Chapter 6 are also provided for readers who want full details about specific parts 5 1 File Tree Overview Target readers beginners The Frama C main directory is split in several sub directories The Frama C source code is mostly provided in directories cil and src The first one contains the source code of Cil 17 It is fortunately quite difficult but not impossible to fall into the worst situation by mistake if you are not a kernel developer 35 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT extended with an ACSL 1 implementation The second one is the core implementation of Frama C This last directory contains directories of the Frama C kernel and directories of the provided Frama C plug in A pretty complete description of the Frama C file tree is provided in Section 6 1 5 2 Configure in Target readers not for standard plug ins developers Prerequisite knowledge of autoconf and shell programming In this Section we detail how to modify the file configure in in order to configure plug ins Frama C configuration has been introduced in Section 2 2 1 and 2 2 4 First Section 5 2 1 introduces the general principle and organisation of configure in Then Section 5 2 2 explains how to configure a new simple plug in without any dependency Next we show how to exhibit dependencies with external libraries and tools Section 5 2 4 and with other plug ins Sec
56. e for a standard plug in and for a kernel integrated plug in are mostly the same The differences between a standard plug in and a kernel integrated one are listed Figure 4 2 Functionality Standard plug in Kernel integrated plug in dynamic linking default possible static linking possible default API in Dynamic possible possible API in Db no possible by modifying the kernel add new abstract types possible possible add new concrete types no possible by modifying the kernel Figure 4 2 Differences between standard plug ins and kernel integrated ones Both kinds of plug ins may be either dynamically linked or statically linked within the Frama C kernel dynamic linking is the standard way for standard plug ins while static linking is the standard way for kernel integrated plug ins Dynamic linking is only available in native mode if you have both Objective Caml 3 11 or higher and a supported architecture for this feature See the Objective Caml manual 14 for additional details Both kinds of plug ins may register their API through module Dynamic but the standard way for kernel integrated plug ins is the use of module Db Kernel integrated plug ins may also declare any types inside the Frama C kernel thanks to the so called Kernel integrated Plug ins 32 44 PLUG INS Types Such types are usable by any plug in and even by some parts of the Frama C kernel However any plug in may still register a new abstract t
57. e html source code generated by make doc see Section 5 18 1 for additional details about this documentation This guide introduces neither the use of Frama C which is the purpose of the user manual 5 nor the use of plug ins which are documented in separated and dedicated manuals 8 6 2 We assume that the reader of this guide already reads the Frama C user manual and knows the main Frama C concepts The reader of this guide may be either a Frama C beginner who just finished reading the user manual and wishes to develop his her own analysis with the help of Frama C an intermediate level plug in developer who wants to better understand one particular aspect of the framework or a Frama C expert who aims to remember details about one specific point of the Frama C development Frama C is fully developed within the Objective Caml programming language aka OCaml 14 Motivations for this choice are given in a Frama C experience report 9 However this guide does not provide any introduction to this programming language the World Wide Web already contains plenty resources for OCaml developers see for instance http caml inria fr resources doc index en html 1 1 About this document To ease reading section heads may state the category of readers they are intended for and a set of prerequisites Appendix A references all the changes made to this document between successive Frama C releases In the index page numbers written in b
58. e return main slice print These directives state that we want to test sparecode and slicing analyses on this file Thus running the following instruction executes two test cases bin ptests byte tests sparecode calls c Dispatch finished waiting for workers to complete Comparisons finished waiting for diffs to complete Diffs finished Summary Run 2 Ok 4 of 4 44 5 6 PLUG IN GENERAL SERVICES 5 5 3 Alternative Testing You may want to set up different testing goals for the same test base Common cases include e checking the result of an analysis with or without an option e checking a preliminary result of an analysis in particular if the complete analysis is costly e checking separately different results of an analysis This is possible with option config of ptests which takes as argument the name of a special test configuration as in bin ptests byte config lt special_name gt plug in Then the directives for this test can be found e inside file tests test_config_ lt special_name gt e inside file tests subdir test_config_ lt special_name gt for each sub directory subdir of tests or e inside each test file in a special comment of the form run config_ lt special_name gt directives All operations for this test configuration should take option config in argument as in bin ptests byte update config lt special_name gt plug in Note that some specific confi
59. e stmt 59 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT A quick look on this code shows that the declaration of the state itself is much more com plicated it uses a functor application but the use of state is simpler Actually what has changed 1 To declare a new internal state apply one of the predefined functors in modules Computation or Cil_computation see interfaces of these modules for the list of avail able modules Here we use StmtHashtbl which provides an hashtable indexed by state ments The type of values associated to statements is a couple of Kernel_function t and Cil_types varinfo The first argument of the functor is the datatype correspond ing to this type see Section 5 11 4 The second argument provides some additional information the initial size of the hashtable an integer similar to the argument of Hashtbl create a name for the resulting state and its dependencies This list of dependencies is built upon values self which are provided by the application of the low level functor Project Computation Register This value is called the kind of the internal state also called state kind and can be used for this purpose Roughly speaking it represents the internal state itself 2 From outside a state actually hides its internal representation in order to ensure some invariants operations on states implementing hashtable does not take an hashtable in argument because they implicitly use the hidden hashtable In ou
60. ebug level 3 If you read this a pp dg 3 let O Db Main extend run Running this example you should see frama c foo debug 2 foo Hello this is Foo Logs foo Try high debug levels you have at least debug 0 foo If you read this you have at least debug 1 Notice that your plug in automatically benefits from its own debug command line parameter and that messages are automatically prefixed with the name of the plug in We now get into more details for an advanced usage of logging services 46 5 7 LOGGING SERVICES 5 7 1 From printf to Log Below is a simple example of how to make a printf based code towards being Log compliant The original code extracted from the Occurrence plugin in Frama C Lithium version is as follows let print one v 1 Format printf variable s 4d n v vname v vid List iter fun ki lv gt Format printf sid fa Za n d ki ki d lval lv eel let print all O compute Occurrences iter print one The transformation is straightforward First you add to all your pretty printing functions an additional Format formatter parameter and you call fprintf instead of printf let print one fmt v 1 Format fprintf fmt variable s 4d n v vname v vid List iter fun ki lv gt Format fprintf fmt sid Za a n d ki ki d Ilval lv al Then you delegate toplevel calls to printf towards an appropriate logging routine with a formatting string contai
61. ecode see Sparecode Status 36 107 INDEX Test 90 Testing 26 Tests Suite 17 Types 17 30 33 52 79 88 90 Wished 81 plugin_types 52 60 Plugin Kernel integrated 81 82 Plugin 14 17 32 45 80 BOOL 62 General_services 64 get_selection 63 INT 63 64 Parameter 63 Register 15 45 46 64 64 debug 46 False 15 64 64 IndexedVal 64 Int 64 result 15 46 String 64 64 True 64 Zero 64 STRING 64 PLUGIN_BFLAGS 88 plugin_BFLAGS 91 PLUGIN_CMI 88 plugin_CMI 91 PLUGIN_CMO 15 19 41 42 88 plugin_CMO 91 PLUGIN_DEPENDS 88 PLUGIN_DEPFLAGS 88 plugin_DEPFLAGS 91 PLUGIN_DIR 19 41 42 88 plugin_DIR 91 PLUGIN_DISTRIB_BIN 90 PLUGIN_DISTRIB_EXTERNAL 90 PLUGIN_DISTRIBUTED 90 PLUGIN_DOCFLAGS 88 plugin_DOCFLAGS 91 PLUGIN_DYNAMIC 42 88 PLUGIN_ENABLE 19 41 42 88 PLUGIN_EXTRA_BYTE 88 PLUGIN_EXTRA_OPT 88 PLUGIN_GENERATED 88 plugin_GENERATED 91 PLUGIN_GUI_CMO 41 73 88 plugin_GUI_OFLAGS 91 PLUGIN_HAS_EXT_DOC 90 PLUGIN_HAS_MLI 21 41 88 PLUGIN_INTERNAL_TEST 90 PLUGIN_INTRO 74 90 plugin_LINK_BFLAGS 91 PLUGIN_LINK_GUI_BFLAGS 88 plugin_LINK_GUI_BFLAGS 91 PLUGIN_LINK_GUI_OFLAGS 88 PLUGIN_LINK_OFLAGS 88 plugin_LINK_OFLAGS 91 PLUGIN_NAME 15 19 21 41 42 74 88 90 PLUGIN_NO_DEFAULT_TEST 90 PLUGIN_NO_TEST 19 21 41 90 PLUGIN_OFLAGS 88 plugin_OFLAGS 91 PLUGIN_TESTS_DIRS 90 plugin_TESTS_DIRS 91 PLUGIN_TESTS_LIB 90 plugin_TESTS_LIB 91 PLUGIN_TYPES
62. ed thanks to Makefile plugin each plug in is packed into a single module PLUGIN_NAME here Hello and we simply export an empty interface for it We also have to explain to Makefile plugin that we use our own interface hello mli for Hello For this purpose in Makefile we add the following line before including Makefile plugin File Makefile 21 CHAPTER 2 TUTORIAL Re Hello A PLUGIN_ENABLE ENABLE_HELLO PLUGIN_NAME Hello PLUGIN_DIR src hello PLUGIN_CMO register PLUGIN_NO_TEST yes PLUGIN_HAS_MLI yes Add this single line include Makefile plugin 2 2 6 Testing Frama C provides a tool called ptests in order to perform non regression and unit tests This tool is detailed in Section 5 5 This section only covers the basic use of ptests First we have to create a test directory for hello mkdir tests hello and in Makefile we have to remove the line PLUGIN_NO_TEST yes File Makefile TAHA tete Hello PARA RAT PLUGIN_ENABLE ENABLE_HELLO PLUGIN_NAME Hello PLUGIN_DIR src hello PLUGIN_CMO register PLUGIN NO TEST yes Remove this single line PLUGIN_HAS_MLI yes include Makefile plugin Now we can add the following test hello c in directory tests hello File tests hello hello c run config OPT hello test of the plug in hello does not require C code anyway It is possible to test the new plug in on this file with the command bin toplev
63. el byte hello tests hello hello c which should display preprocessing running gcc C E I tests hello c Hello Frama C World The specific output of the plug in hello is the last line It is also possible to use ptests to run tests automatically bin ptests byte hello The above command runs the Frama C toplevel on each C file contained in the directory tests hello For each of them it also uses directives following run config given at the top of files Here for the test tests hello hello c the directive specifies that the toplevel has to be executed with the option hello Below is the output of this command 22 2 2 KERNEL INTEGRATED PLUG IN Dispatch finished waiting for workers to complete System error while comparing Maybe one of the files is missing tests hello result hello res log or tests hello oracle hello res oracle System error while comparing Maybe one of the files is missing tests hello result hello err log or tests hello oracle hello err oracle Comparisons finished waiting for diffs to complete Diffs finished Summary Run 1 Ok 0 of 2 This result says that testing fails because it is not possible to compare the execution results with previously stored results oracles You have to execute bin ptests byte update hello Thus each time one executes ptests byte differences with the saved oracles are displayed Furthermore you can easily check whether the changes in plug in hel
64. en proceed as described above References to specific files in the plugin source directory should be guarded with the following macro PLUGIN_RELATIVE_PATH file 39 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT If the external plugin has some dependencies as described in sections 5 2 4 and 5 2 5 the configure script configure must check that all dependencies are met This is done with the following macro check_plugin_dependencies An external plugin can have dependencies upon previously installed plugins However two separately installed plugins can not be mutually dependent on each other Nevertheless they can be compiled together with the main Frama C sources using the enable external option of configure see section 5 4 3 for more details Finally the configuration must end with the following command write_plugin_config files where files are the files that must be processed by configure as in AC_CONFIG_FILES macro PLUGIN_RELATIVE_PATH is unneeded here 5 3 Makefile Target readers not for standard plug in developers Prerequisite knowledge of make In this section we detail the use of Makefile dedicated to Frama C compilation This file is split in several sections which are described in Section 6 3 2 By default executing make only displays an overview of commands For example here is the output of the compilation of source file src kernel db cmo make src kernel db cmo Ocamlc src kernel db cmo
65. es even the Frama C version of Cil which are shortly described below 31 CHAPTER 4 SOFTWARE ARCHITECTURE Module Log provides an uniform way to display user messages in Frama C e Module Cmdline parses the Frama C command line e Module Plugin provides a high level API on top of the two previous modules for the plug in developer a developer usually uses this module and does not directly use mod ules Log or Cmdline e Module Type is a library handling OCaml types as first class values Such values are required by journalization and registration of dynamic values See section 5 8 for details e Module Journal handles how Frama C journalizes its actions See section 5 9 for details e In directory src project the Frama C kernel embeds a library called Project which permits the consistency of results for multi analysis of multi ASTs in a dynamic setting See section 5 11 for details 4 4 Plug ins In Frama C plug ins are analysis or source to source transformations Each of them is an extension point of the Frama C kernel Frama C allows plug in collaborations a plug in p can use a list of plug ins p1 pn and conversely Mutual dependences between plug ins are even possible If a plug in is designed to be used by another plug in its API has to be registered either in module Dynamic or in module Db This last method is only available to kernel integrated plug ins More generally the set of functionalities availabl
66. ex html The html pages belonging to the directory doc www src must not be used in order to display the website because relative links are not the same than those of the real website Use html pages of directory doc www export instead Recommendation 5 6 You can use the address http validator w3 org tvalidate_ by_ upload in order to check the validity of your html code For this purpose you can use make all instead of make html_pages If you want to officially put the webpage on the Frama C website you have to contact CEA 5 19 License Policy Target readers developers with a SVN access 75 Prerequisite CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT knowledge of make If you want to redistribute a plug in inside Frama C you have to define a proper license policy For this purpose some help is provide in the Makefile Mainly we distinguish two cases described below e If the wished license is already used inside Frama C just extend the variable corresponding to the wished license in order to include files of your plug in Next run make headers Example 5 29 Plug in slicing is released under LGPL and is proprietary of both CEA and INRIA So in the makefile there is the following line CEA_INRIA_LGPL src slicing_types ml src slicing ml e If the wished license is unknown inside Frama C you have to 1 Add a new variable v corresponding to it and assign files of your plug in 2 Extend va
67. f the basic ones log kind verbose debug lt options gt Emits a message with the given kind when the verbosity and or debugging level are sufficient 49 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT with log f kind lt options gt Emits a message like log and finally pass the generated message to the continuation f and returns its result The default kind is Result but all the other kind of message can be specified For verbosity and debugging levels the message is emitted when log verbosity is at least 1 log verbose n verbosity is at least n log debug n debugging is at least n log verbose v debug d either verbosity is at least v or debugging is at least d Channel Management The logging services are build upon channels which are basically buffered formatters to standard output extended with locking delayed echo and notification services The very safe feature of logging services is that recursive calls are protected A message is only echoed upon termination and a channel buffer is stacked only if necessary to preserve memory Services provided at plugin registration are convenient shortcuts to low level logging service onto channels The Log interface allows you to create such channels for your own purposes Basically channels ensure that no message emission interfere with each others during echo on standard output Hence the forbidden direct access to Pervasives stdout However Log i
68. files e Makefile dynamic_confic this Makefile is automatically generated either from Makefile dynamic_config internal or Makefile dynamic_config external It sets variables which automatically configure Makefile dynamic e Makefile kernel is automatically generated from Makefile It contains several vari ables 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 6 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 and rules are defined in Makefile common which includes Makefile config in 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 plug ins with their own Makefiles 6 3 2 Sections of Makefile Makefile config in and Makefile common Figure 6 7 presents the different parts of Makefile config in Makefile common and Makefile in the order that they are introduced in these files The third row of the tabu lar says whether the given part may be modified by a kernel integrated plug in developer More details are provided belo
69. gic Type System 79 Logic_const 79 prel 71 tern 71 Logic_typing 79 Logic_utils expr_to_term 71 Loop 80 Lil to _acsl 42 Makefile 17 19 21 40 73 74 76 77 82 82 83 Makefile common 82 Makefile config in 40 82 83 Makefile dynamic 14 15 17 41 41 42 82 83 88 Makefile dynamic_config 82 Makefile dynamic_config external 82 Makefile dynamic_config internal 82 Makefile kernel 82 Makefile plugin 19 40 82 83 88 memo 59 Memoization 54 56 59 60 Memory State 30 31 Memory States Toolbox 79 memory_states 79 Messages 46 106 misc 79 Module Initialization see Initialization ocamlgraph 78 Occurrence 37 73 only 62 63 Oracle 22 43 44 92 Parameters 63 Parameters 63 80 CodeOutput 51 Dynamic 65 Dynamic Bool 65 UseUnicode 64 Parsing 30 31 Pdg 61 PdgTypes Pdg Datatype 61 Platform 81 Plug in 13 29 32 Access 53 API 26 53 Architecture 25 Command Line Options 25 Compilation 86 Compiled 78 Database see Db Dependency 36 36 39 81 88 Directory 18 73 88 Distribution 90 Documentation 27 74 74 88 90 GUI 14 17 26 39 66 73 88 Hello see Hello Implementation 79 Initialization see Initialization Interface 17 18 21 74 88 Kernel integrated 13 16 32 Access 52 Registration 52 License 76 Makefile 26 Messages 25 Name 88 Occurrence see Occurrence Pdg see Pdg Registration 25 53 Script 25 Slicing see Slicing Spar
70. gister the new Frama C option hello x module Enabled Self False struct let option name hello let help pretty print Hello world let kind Correctness end let print O Self result Hello world The code below is not mandatory you can ignore it in a first reading It provides an API for the plug in so that the function run is callable by Both files are distributed within Frama C and they are available from the directory src dummy hello_world of the source distribution 15 CHAPTER 2 TUTORIAL another plug in and journalized first each plug in can call Dynamic get Hello run Datatype func Datatype unit Datatype unit in order to call run and second each call to run is written in the Frama C journal let print Dynamic register plugin Hello run journalize true Datatype func Datatype unit Datatype unit print Print Hello World whenever the option is set x let run if Enabled get then print Register the function run as a main entry point let Db Main extend run 2 2 Kernel integrated Plug in Writing a plug in this way is deprecated except for very specific tasks Before writing a kernel integrated plug in you must be sure that it is not possible to write it in the standard way described in the previous section This section is out of date Please report as feature request on http bts frama c com if you
71. gurations require dynamic linking which is not available on all platforms for native code ptests takes care of reverting to bytecode when it detects that the OPT or EXECNOW options of a test require dynamic linking This occurs currently in the following cases e OPT contains the option load script e OPT contains the option load module e EXECNOW use make to create a cmxs 5 6 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 the features of Frama C Second it provides to the end user a common set of features for 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 5 9 Here is how the plug in From applies the functor Plugin Register for its own use 45 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT include Plugin Register struct let name from analysis let shortname from let descr 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 5 7 Second it allows to define plug in specific parameters available as option on the Frama C command line for the end user see Section 5 12 5 7 Logging Services Displaying results of plug in computations to
72. he Frama C toplevel on each specified test which are usually C files Specific directives can be used for each test Each result of the execution is compared from the previously saved result called the oracle A test is successful if and only if there is no difference Actually the number of results is twice that the number of tests because standard and error outputs are compared separately First Section 5 5 1 shows how to use ptests Next Section 5 5 2 explains how to use predefined directives to configure tests Last Section 5 5 3 describes how to set up various testing goals for the same test base 5 5 1 Using ptests The simplest way of using ptests is through make tests which is roughly equivalent to time bin ptests byte This command runs all the tests belonging to a sub directory of directory tests ptests also accepts specific test suites in arguments A test suite is either a name of a sub directory in directory tests or a filename with its complete path Example 5 6 If you want to test plug in sparecode and specific test tests pdg variadic c just run bin ptests byte sparecode tests pdg variadic c which should display if there are 7 tests in directory tests sparecode Dispatch finished waiting for workers to complete Comparisons finished waiting for diffs to complete Diffs finished Summary Run 8 Ok 16 of 16 ptests accepts different options which are used to customize test sequences These optio
73. he non gui modules of p are always linked before the gui modules of p 3 finally the module Boot is linked at the very end of this stage Plug in developers can not customize this stage In particular the module Cmdline one of the first linked modules see Figure 4 1 performs a very early configuration stage such as checking if journalization has to be activated cf Section 5 9 or setting the global verbosity and debugging levels The Early Stage this stage initializes the kernel services More precisely a first the default project is created b then the parsing of command line options registered for the Cmdline Early stage c finally all functions registered through Cmdline run_after_early_stage are exe cuted in an unspecified order The Extending Stage the searching and loading of dynamically linked plug ins of journal scripts and modules is performed at this stage More precisely a the command line options registered for the Cmdline Extending stage are treated such as load journal and add path b the hooks registered through Cmdline run_during_extending_stage are executed Such hooks include kernel function calls for searching loading and linking the various plug ins journal and scripts compilation units with respect to the command line options parsed during stages B and C The Running Phase the command line is split into several groups of command line arguments each of them separated by an optio
74. he visit will stop but the information associated to the old value will be associated to the new one If the children are to be visited it is undefined whether the table entries are visited before or after the children in the AST 5 14 7 Example This example is out of date Please report as feature request on http bts frama c com if you really need it 70 5 15 LOGICAL ANNOTATIONS Here is a small copy visitor that adds an assertion for each division in the program stating that the divisor is not zero open Cil types open Cil class non zero divisor prj object self inherit Visitor generic frama c visitor prj Cil copy visit x A division is an expression we override the vexpr method method vexpr e match e enode with BinOp DiviMod e2 gt let t Cil typeOf e2 in let logic e2 Logic const term TCastE t Logic utils expr to term cast true e2 Ctype t in let assertion Logic const prel Rneq logic e2 Cil lzero in x At this point we have built the assertion we want to insert It remains to attach it to the correct statement The cil visitor maintains the information of which statement is currently visited in the current stmt method which returns None when outside of a statement e g when visiting a global declaration Here it necessarily returns Some let stmt Extlib the self current stmt in Since we are copying the file in a new project we can t insert the annotation into
75. hich files in the direc tory containing the current test suite are actually part of the suite This directive is only usable in a test_config configuration file 94 Appendix Changes This chapter summarizes the major changes in this documentation between each Frama C release First we list changes of the last release e Tutorial of the Future new chapter for preparing a future tutorial e Types as first class values links to articles e Tutorial kernel integrated plug ins are now deprecated e Visitors example is now out of date Carbon 20101201 betal e Visitors update example to new kernel API e Documentation external plugin API documentation e Visitors fix bug replace DoChildrenPost by ChangeDoChildrenPost change seman tics wrt vstmt_aux Carbon 20101201 betal e Very Important Preliminary Warning adding this very important chapter e Tutorial fix bug in the Hello World example e Testing updated semantics of CMD and STDOPT directives e Initialization Steps updated according to new options then and then on and to the new Files Setting stage e Visitors example updated We list changes of previous releases below 95 APPENDIX A CHANGES Boron 20100401 Configure in updated Tutorial the section about kernel integrated plug in is out of date Project no more rehash in datatypes Initialisation Steps fixed according to the current implementation Plug in Registr
76. ial_name gt e inside file tests subdir test_config_ lt special_name gt for each sub directory subdir of tests or e inside each test file 92 6 4 TESTING Kind Name Specification default CMD Program to run bin toplevel opt OPT Options given to the program val out input deps Command STDOPT Add and remove options from None the default set EXECNOW Run a command before the None following commands FILTER Command used to filter re None sults mse ates DONTRUN Do not execute this test None FILEREG selects the files to test EAN Mic COMMENT Comment in the configuration None GCC Unused compatibility only None Figure 6 12 Directives in configuration headers of test files For a given test tests suite test ml each existing file in the sequence above is read in order and defines a configuration level the default configuration level always exists e CMD allows to change the command that is used for the following OPT directives until a new CMD directive is found No test case is generated if there is no further OPT directive At a given configuration level the default value for directive CMD is the last CMD directive of the preceding configuration level e If there are several directives OPT in the same configuration level they correspond to different test cases The OPT directive s of a given configuration level replace s the ones of the preceding level e The STD
77. ide p for instance in another plug in requires the use of module Parameters Dynamic because the module defining the parameter is not visible from the outside of its plug in so the option is accessible by any other plug ins and by the Frama C kernel as well Functions of sub modules of module Parameters Dynamic takes a string in argument which is the option name associated with the parameter Example 5 28 Outside the plug in From just write Parameters Dynamic Bool get calldeps in order to know whether callsite wise dependencies has been required 5 13 Initialization Steps Prerequisite knowledge of linking of OCaml files In a standard way Frama C modules are initialized in the link order which remains mostly unspecified so you have to use side effects at module initialization time carefully This section details the different stages of the Frama C boot process to help advanced plug in developers interact more deeply with the kernel process It can be also useful for debugging initialization problems As a general rule plug in routines must never be executed at link time Any useful code be it for registration configuration or C code analysis should be registered as function hooks to be executed at a proper time during the Frama C boot process see Section 5 11 5 In general a hook does nothing except when some parameters have been positioned These parameters comes from the command line see Section 5 12 or fro
78. ien Doligez Hashconsing in an incrementally garbage collected system a story of weak pointers and hashconsing in ocaml 3 10 2 In ACM SIGPLAN Workshop on ML Victoria British Columbia Canada September 2008 Pascal Cuoq and Virgile Prevosto Frama C s value analysis plug in February 2011 http frama c cea fr download value analysis pdf Pascal Cuoq and Julien Signoles Experience Report OCaml for an industrial strength static analysis framework In Proceedings of International Conference of Functional Pro gramming ICFP 09 pages 281 286 New York NY USA September 2009 ACM Press Andrey P Ershov On programming of arithmetic operations Communication of the ACM 1 8 3 6 1958 Free Software Foundation GNU make April 2006 http www gnu org software make manual make html Flavors Jacques Garrigue Benjamin Monate Olivier Andrieu and Jun Furuse LablGTK2 http wwwfun kurims kyoto u ac jp soft olabl lablgtk html Eiichi Goto Monocopy and Associative Algorithms in Extended Lisp Technical Report TR 74 03 University of Toyko 1974 99 14 15 16 17 18 19 20 BIBLIOGRAPHY Xavier Leroy Damien Doligez Jacques Garrigue Didier R my and J r me Vouillon The Objective Caml system http caml inria fr pub docs manual ocaml index html Donald Michie Memo functions a language feature with rote learning properties Research Memorandum MIP R 29 Department of Machine
79. iff and cmp options play two related but distinct roles cmp is always used for each test in fact it used twice one for the standard output and one for the error output Only its exit code is taken into account by ptests and the output of cmp is discarded An exit code of 1 means that the two files have differences The two files will then be analyzed by diff whose role is to show the differences between the files An exit code of 0 means that the two files are identical Thus they won t be processed by diff An exit code of 2 indicates an error during the comparison for instance because the corresponding oracle does not exist Any other exit code results in a fatal error It is possible to use the same command for both cmp and diff with the use diff as cmp option which will take as cmp command the command used for diff The exclude option can take as argument a whole suite or an individual test It can be used with any behavior Any directive can identify a file using a relative path The default directory considered for is always the parent directory of directory tests The DONTRUN directive does not need to have any content but it is useful to provide an explanation of why the test should not be 91 CHAPTER 6 REFERENCE MANUAL kind Name Specification Default add options Additional options passed to the Toplevel toplevel byte Use bytecode toplevel no opt Use native toplevel yes run Delete current
80. ing Makefile no 31 Cleaning Makefile no 32 Depend Makefile no 33 ptests Makefile no 34 Source distribution Makefile no Figure 6 7 Sections of Makefile config in Makefile common and Makefile 84 10 11 12 13 6 3 MAKEFILES Working directories splitted between Makefile config in and Makefile common defines the main directories of Frama C In particular it declares the variable UNPACKED_DIRS which should be extended by a plug in developer if he uses files which do not belong to the plug in directory that is if variable PLUGIN_TYPES_CMO is set see Section 6 3 3 Installation paths defines where Frama C has to be installed Ocaml stuff defines the Objective Caml compilers and specific related flags Libraries defines variables for libraries required by Frama C Miscellaneous commands defines some additional commands Miscellaneous variables defines some additional variables Variables for plug ins defines some variables used by plug ins distributed within Frama C and using the configure of Frama C Flags defines some variables setting compilation flags Verbosing sets how make prints the command In particular it defines the variable VERBOSEMAKE which must be set yes in order to see the full make commands in the user console The typical use is make VERBOSEMAKE yes Shell commands sets all the shell commands eventually executed while calling make Command pretty p
81. internal states for which registration is detailed in Sections 5 11 4 5 11 5 and 5 11 6 Section 5 11 4 is dedicated to so called datatypes Section 5 11 5 is dedicated to the internal states themselves Section 5 11 6 is dedicated to low level registration Finally Section 5 11 7 shows how to handle projects and internal states in a clever and proper way 5 11 1 Overview and Key Notions In Frama C many mostly global data are attached to an AST For example there are the AST itself options of the command line see Section 5 12 and tables containing results of analyses Frama C extensively uses memoization 15 16 in order to avoid re computating analyses The set of all these data is called a project It is the only value savable on the disk and restorable by loading Several ASTs can exist at the same time in Frama C and thus several projects as well there is one AST per project Besides each data has one value per AST thus there are as many values for each data as projects ASTs 54 5 11 PROJECT MANAGEMENT SYSTEM The set of all the projects stands for the internal state of Frama C it consists of all the ASTs defined in Frama C and for each of them the corresponding values of all the attached data A related notion is internal state of a data d That is the different values of d in projects for each data the cardinal of this set is equal to the cardinal of the internal state of Frama C i e the number of existing projects
82. istering the value and the second one is a binding name of the registered OCaml value It must not be used for value registration anywhere else in the Frama C world It is required for another plug in in order to access to this value see next paragraph The third argument is the so called type value of the registered value i e an OCaml value representing its type see Section 5 8 for additional details It is required for safety reasons when accessing to the registered value see the next paragraph Predefined type values exist in modules Type for usual OCaml types like int and Kernel_type for usual Frama C types such as Cil_types varinfo The third argument is the value itself Example 5 13 Here is how the function run of the plug in hello of the tutorial is registered The type of this function is unit unit let run unit let O Dynamic register plugin Hello run Type func Type unit Type unit run If the string Hello run is already used to register a dynamic value then the exception Type AlreadyExists is raised during plug in initialization see Section 5 13 4A direct consequence is that you cannot use the whole Frama C functionalities such as module Db inside this code 53 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT The function call Type func Type unit Type unit returns the type value of unit unit Note that because of the type of Dynamic register and the types of its arguments the OCaml
83. it is a boolean parameter initialized by default to false The declared interface for this module is simply module Print Plugin INT Another example is the parameter corresponding to the option security lattice of the plug in security is the module Lattice defined in the file src security options ml It is implemented as follow module Lattice String struct let option name security lattice let default weak let arg name let descr specify security lattice end So it is a string parameter initialized by default to the string weak The field arg_name is set to the empty string so a default name for the argument of this option will be choose by Frama C while displaying the help of this parameter The field descr is the help message The Interface for this module is simple module Lattice Plugin STRING Recommendation 5 3 Parameters of a same plug in plugin should belong to a module called Options or Plugin_options inside the plug in directory Using a kernel parameters of a parameter of your own plug in is very simple you have simply to call the function get corresponding to your parameter 64 5 13 INITIALIZATION STEPS Example 5 27 To know whether Frama C uses unicode just write Parameters UseUnicode get O Inside the plug in From just write From_parameters ForceCallDeps get O in order to know whether callsite wise dependencies has been required Using a parameter of a plug in p outs
84. level is used level n minimal level required is n Source Options By default a message is not localized You may specify a source location either specifically or by using the current location of an AST visitor source s use the source location s see Log mli current true use the current source location managed by Cil CurrentLoc Emission Options By default a message is echoed to the user after its construction and 1t is sent to registered callbacks when emitted See Section 5 7 4 below for more details on how to globally modify such a behavior During the message construction you can locally modify the emission process with the following options 48 5 7 LOGGING SERVICES emitwith f suppresses the echo and sends the emitted event only to the callback func tion f Listeners are not fired at all once true finally discards the message if the same one was already emitted before with the once option Append Option All logging routines have the append f optional parameter where f is function taking a Format formatter as parameter and returning unit This function f is invoked to append some text to the logging routine Such continuation passing style is sometime necessary for defining new polymorphic formatting functions It has been introduced for the same purpose than standard Format kfprintf like functions 5 7 4 Advanced Logging Services Message Emission During message construction the message content i
85. linked within Frama C here no says that the plug in will be statically linked Now we are ready to execute autoconf configure and to check that the new plug in hello is going to compile you should have the line checking for src hello yes hello yes in the configuration summary Compilation Once configure in is extended we also have to modify Makefile with the following lines File Makefile 4In this document a comment containing among lines of code represents an undisplayed piece of code written either previously in the document or by someone else 19 CHAPTER 2 TUTORIAL Add the following lines after other plug ins compilation directives in the section Plug in sections HELPER Hello PLUGIN_ENABLE ENABLE_HELLO PLUGIN_NAME Hello PLUGIN_DIR src hello PLUGIN_CMO register PLUGIN_NO_TEST yes include Makefile plugin These lines use the predefined makefile Makefile plugin which is a generic makefile dedicated to the compilation of plug ins There are more than twenty variables than can be used to customize the behavior of Makefile plugin These variables are all described in Section 6 3 3 but most of them have reasonable default values so that it is not necessary to describe more than the few ones above PLUGIN_ENABLE indicates that the plug in should be compiled Here we use the variable ENABLE_HELLO set by configure in e PLUGIN_NAME is the name of the plug in
86. lo are compliant with all existing tests For example if we execute one more time bin ptests byte hello Diffs finished Summary Run 2 Ok 2 of 2 This indicates that everything is alright Finally you can also check if your changes break something else in the Frama C kernel or in other plug ins by executing ptests on all default tests with make tests Note to SVN users If you have write access to the SVN repository you may commit your changes into the archive Before that you have to perform non regression tests in order to ensure that your modifications do not break the archive So you must execute the following commands svn add Do not forget new oracles svn up make tests emacs Changelog svn commit m informative message If you created any new files use the svn add command to add them into the archive The svn up command updates your local directory with respect to the root repository The make tests command performs the non regression tests Finally if and only if the regression tests do not expose any problem update the file Changelog according to your changes and commit them thanks with the svn commit command 2 2 7 Copyright your Work Target readers developers with SVN access If you want to redistribute your plug in you have to choose a license policy for it compatible with Frama C Section 5 19 provides details on how to proceed Here suppose we want to put the plug in hello unde
87. low on a given statement etc Typical options include current true to localize the message on the current source location error lt options gt abort lt options gt Use these routines for reporting to the user an error in its inputs It can be used for non valid parameters for instance It should not be used for some not yet implemented feature however The abort routine is a variant that raises an exception and thus aborts the computation failure lt options gt fatal lt options gt Use these routines for reporting to the user that your plug in is now in inconsistent state or can not continue its computation Typically you have just discovered a bug in your plug in The fatal routine is a variant that raises an exception verify condition lt options gt First the routine evaluates the condition and the formatting arguments then discards the message if the condition holds and displays a message otherwise Finally it returns the condition value A typical usage is for example assert verify x gt 0 Expected a positive value 4d x 5 7 3 Logging Routine Options Logging routines have optional parameters to modify their general behavior Hence their involved type in Log mli Level Option A minimal level of verbosity or debugging can be specified for the message to be emitted For the result and feedback channels the verbosity level is used for the debug channel the debugging
88. m the configuration panel of the GUI However from the initialization process point of view both source of parameters are treated as command line ones Thus registering and executing a hook is tightly coupled with handling the command line parameters The parsing of the command line parameters is performed in several phases and stages each one dedicated to specific operations For instance journal replays should be performed after loading dynamic plugins and so on Following the general rule stated at the beginning of this section even the kernel services of Frama C are internally registered as hooks routines to be executed at a specific stage of the initialization process among plug ins ones From the plug in developer point of view the hooks are registered by calling the run_after_xxx_stage routines in Cmdline module and extend routine in the Db Main mod ule The initialization phases and stages of Frama C are described below in their execution order 65 A C CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT The Initialization Stage this stage initializes Frama C compilation units following some partially specified order More precisely 1 the architecture dependencies depicted on Figure 4 1 cf p 29 are respected In particular the kernel services are linked first then the kernel integrated types for plug ins and finally the plug ins are linked in unspecified order 2 when the GUI is present for any plug in p t
89. mentation bin Binaries concimied Tiles lib Some compiled files doc Documentation directory Documentations headers Headers of source files Section 5 19 licenses Licenses used by plug ins and kernel Section 5 19 Shared libraries share Shared files Figure 6 1 Frama C directories e The Frama C root directory contains the configuration files the main Makefile and some information files in uppercase 17 CHAPTER 6 REFERENCE MANUAL Frama C sources are split in four directories sre described in Section 6 1 2 contains the core of the implementation while cil described in Section 6 1 1 ocamlgraph and external respectively contains the implementation of Cil extended with ACSL a version of the OcamlGraph library 4 compatible within Frama C and external libraries included in the Frama C distribution e The directory tests contains the Frama C test suite which is used by the ptests tool see Section 5 5 e Directories bin and lib contain binary files mainly produced by Frama C compila tion Frama C executables belong to the directory bin the directories 1ib plugins and lib gui receive the compiled plug ins and the directory lib fc receives the compiled kernel interface You should never add yourself any file in these directories e Documentation including plug in specific source code and ACSL documentations is provided in directory doc Directories headers and licenses contains files useful for copyright
90. module name of the plug in This name must be capitalized as is each OCaml module name e Variable PLUGIN_DIR is the directory containing plug in source files It is usually set to src plugin where plugin is the plug in name e Variable PLUGIN_ENABLE must be set to yes if the plug in has to be compiled It is usually set to plugin_ENABLE provided by configure in where plugin is the plug in name e Variable PLUGIN_DYNAMIC must be set to yes if the plug in has to be dynamically linked with Frama C e Variable PLUGIN_HAS_MLI must be set to yes if plug in plugin gets a file mli which must be capitalized Plugin mli see Section 5 18 describing its API Note that this API should be empty in order to enforce the architecture invariant which is that each plug in is used through Db see Chapter 4 e Variables PLUGIN_CMO and PLUGIN_CMI are respectively cmo plug in files and cmi files without corresponding cmo plug in files For each of them do not write their file path nor their file extension they are automatically added PLUGIN_DIR f cm io for a file f e Variable PLUGIN_TYPES_CMO is the cmo plug in files which do not belong to PLUGIN_DIR They usually belong to src plugin_types where plugin is the plug in name see Section 5 10 1 Do not write file extension which is cmo it is automatically added e Variable PLUGIN_GUI_CMO is the cmo plug in files which have to be linked with the GUI see Section 5 17 As for vari
91. modules are shown in Figure 6 4 e Directory logic is the logic toolbox It contains modules helping to handle logical annotations and their status e Directories ai and memory_states are the abstract interpretation and memory state toolboxes see section 5 16 In particular in ai module Abstract_interp defines useful generic lattices and module Ival defines some pre instantiated arithmetic lat tices while in memory_states module Locations provides several representations of C locations and modules Lmap and Lmap_bitwise provide maps indexed by such locations e Directory project is the project library fully described in Section 5 11 e Directories lib and misc contain datastructures and operations used in Frama C In particular module Extlib is the Frama C extension of the OCaml standard library whereas module Type is the interface for type values the OCaml values representing OCaml types required by dynamic plug in registrations and uses and journalization see Section 5 8 79 CHAPTER 6 REFERENCE MANUAL Kind Name Specification Reference AST Ast The Cil AST for Frama C Ast_info Operations over the Cil AST File AST creation and access to C files Globals Operations on globals Global i f abs Kernel_function Operations on functions Annotations Operations on annotations Loop Operations on loops Db Static plug in database Section 5 10 1 Database Db_types Type declarations required by Db Secti
92. n then or an option then on p thus if there is n occurrences of then or then on p then there are n 1 groups For each group the following stages are executed in sequence all the stages are executed on the first group provided on the command line then they are executed on the second group and so on 1 The Extended Stage this step is reserved for commands which require that all plug ins are loaded but which must be executed very early More precisely a the command line options registered for the Cmdline Extended stage are treated such as verbose and debug b the hooks registered through Cmdline run_after_extended_stage Most of these registered hooks come from postponed internal state dependencies see Section 5 11 5 Remark that both statically and dynamically linked plug ins have been loaded at this stage Verbosity and debug level for each plug in are determined during this stage 2 The Exiting Stage this step is reserved for commands that makes Frama C exit before starting any analysis at all such as printing help informations 66 5 14 VISITORS a the command line options registered for the Cmdline Exiting stage are treated b the hooks registered through Cmdline run_after_exiting_stage are executed in an unspecified order All these functions should do nothing using Cmdline nop or raise Cmdline Exit for stopping Frama C quickly 3 The Loading Stage this is where the initial state of Frama C c
93. ning the necessary t and a formatters let print all O compute result t fun fmt Occurrences iter print one fmt 5 7 2 Log Quick Reference The logging routines for your plugins consist in an implementation of the Log Messages inter face which is included in the Plugin S interface returned by the registration of your plugin The main routines of interest are result lt options gt Outputs most of your messages with this routine You may specify level n option to discard too detailed messages in conjunction with the verbose command line option The default level is 1 feedback lt options gt Reserved for short messages that gives feedback about the progression of long compu tations Typically entering a function body or iterating during fixpoint computation The level option can be used as for result debug lt options gt To be used for plug in development messages and internal error diagnosis You may specify level n option to discard too detailed messages in conjunction with the debug command line option The default message level is 1 and the default debugging level is 0 Hence without any option debug discards all its messages warning lt options gt For reporting to the user an important information about the validity of the analysis 47 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT performed by your plug in For instance if you locally assume non arithmetic overf
94. notification see Section 5 19 e Directory share contains useful libraries for Frama C users such as the Frama C C library e g ad hoc libraries such as 1ibc and malloc for Frama C as well as user oriented Makefiles 6 1 1 The cil directory The source files of Cil belong to the five directories shown in Figure 6 2 More details are provided below Name Specification ocamlutil OCaml useful utilities src Main Cil files src ext Syntactic analysis provided by Cil src frontc C frontend src logic ACSL frontend Figure 6 2 Cil directories e ocamlutil contains some OCaml utilities useful for a plug in developer The most important modules are Inthash and Cilutil The first one contains an implementation of hashtables optimized for integer keys while the second one contains some useful functions e g out_some which extracts a value from an option type and datastructures e g the module StmtHashtb1 which implements hashtables optimized for statement keys e src contains the main files of Cil The most important modules are Cil_types and Cil The first one contains type declarations of the Cil AST while the second one contains useful operations over this AST e src ext contains syntactic analysis provided by Cil For example module Cfg pro vides control flow graph module Callgraph provides a syntactic callgraph and module Dataflow provides parameterized forward backward data flow analysis 78 6 1 F
95. ns are detailed in Section 6 4 43 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT Example 5 7 If the code of plug in plug in has changed a typical sequence of tests is the following one bin ptests byte plug in bin ptests byte update plug in make tests So we first run the tests suite corresponding to plug in in order to display what tests have been modified by the changes After checking the displayed differences we validate the changes by updating the oracles Finally we run all the test suites in order to ensure that the changes do not break anything else in Frama C 5 5 2 Configuration In order to exactly perform the test that you wish some directives can be set in three different places We indicate first these places and next the possible directives The places are e inside file tests test_config e inside file tests subdir test_config for each sub directory subdir of tests or e inside each test file in a special comment of the form run config directives In each of the above case the configuration is done by a list of directives Each directive has to be on one line and to have the form CONFIG_OPTION value There is exactly one directive by line The different directives e possibilities for CONFIG_OPTION are detailed in Section 6 4 Example 5 8 Test tests sparecode calls c declares the following directives run config OPT sparecode analysis OPT slicing level 2 slic
96. nt computed true O print computed false with Project IOError _ gt exit 1 It displays false true false 5 11 3 Internal State Principle If a data should be part of the internal state of Frama C you must register it as an internal state also called a computation because it is often related to memoization Here we first explain what are the functionalities of each internal state and then we present the general principle of registration Internal State Functionalities Whenever you want to attach a data e g a table containing results of an analysis to an AST you have to register it as an internal state The main functionalities provide to each internal state are the following e It is automatically updated whenever the current project changes so your data is always consistent with the current project 56 5 11 PROJECT MANAGEMENT SYSTEM e It is part of the information saved on disk for restoration in a later session e It may be part of a selection which is roughly speaking a set of internal states Which such a selection you can control which internal states project operations are applied on see Section 5 11 7 For example it is possible to clear all the internal states which depend of the value analysis e It is possible to ensure inter analysis consistency by setting internal state dependen cies For example if the entry point of the analysed program is changed using Globals set_entr
97. nterface allows you to create such channels on your own in addition to the one automatically created for your plug in new channel name This creates a new channel There is only one channel per name and the function returns the existing one if any Plug in channels are registered under their short name and the kernel channel is registered under Log kernel_channel_name log channel channel kind prefix lt options gt This routine is similar to the log one with_log channel channel f kind prefix lt options gt This routine is similar to the with_log one With both logging routines you may specify a prefix to be used during echo The available switches are Label t use the string t as a prefix for the first echoed line of text then use an inden tation of same length for the next lines Prefix t use the string t as a prefix for all lines of text Indent n use an indentation of n spaces for all lines of text When left unspecified the prefix is computed from the message kind and the channel name like for plug ins 50 5 8 TYPES AS FIRST CLASS VALUES Output Management It is possible to ask Log to redirect its output to another channel set output out flush The parameters are the same than those of Format make_formatter out outputs a sub string and flush actually writes the buffered text to the underlying device It is also possible to have a momentary direct access to Pervasives stdout or whateve
98. ogic_info_decl and vlogic_info_use logic_type_info vlogic_type_info_decl and vlogic_type_info_use and logic_ctor_info vlogic_ctor_info_decl and vlogic_ctor_info_use More detailed information can be found in cil mli For the Frama C visitor two methods vstmt and vglob take care of maintaining the coherence between the transformed AST and the internal state of Frama C Thus they must not be redefined One should redefine vstmt_aux and vglob_aux instead 5 14 3 Action Performed The return value of visiting methods indicates what should be done next There are six possibilities e SkipChildren the visitor does not visit the children e ChangeTo v the old node is replaced by v and the visit stops e DoChildren the visit goes on with the children this is the default behavior 10This naming convention is not strictly enforced For instance the method corresponding to offset is voffs 68 5 14 VISITORS e JustCopy is only meaningful for the copy visitor Indicates that the visit should go on with the children but only perform a fresh copy of the nodes e ChangeToPost v f the old node is replaced by v and f is applied to the result This is however not exactly the same thing as returning ChangeTo f v Namely in the case of vglob_aux f will be applied to v only after the operations needed to maintain the consistency of Frama C s internal state with respect to the AST have been per formed Thus ChangeToPost should be used
99. old italics e g 1 reference the defining sections for the corresponding entries while other numbers e g 1 are less important references 11 CHAPTER 1 INTRODUCTION Furthermore the name of each OCaml value in the index corresponds to an actual Frama C value In the Frama C source code the ocamldoc documentation of such a value contains the special tag plugin development guide while in the html documentation of the Frama C API the note Consult the Plugin Development Guide for additional details is attached the value name The most important paragraphs are displayed inside gray boxes like this one A plug in developer must follow them very carefully There are numerous code snippets in this document Beware that copy pasting them from the PDF to your favorite text editor may prevent your code from compiling because the PDF text can contain non ASCII characters 1 2 Outline This guide is organised in four parts Chapter 2 is a step by step tutorial for developing a new plug in within the Frama C plat form At the end of this tutorial a developer should be able to extend Frama C with a simple analysis available as a Frama C plug in Chapter 4 presents the Frama C software architecture Chapter 5 details how to use all the services provided by Frama C in order to develop a fully integrated plug in Chapter 6 is a reference manual with complete documentation for some particular points of the Frama C platform
100. on 5 10 1 Dynamic Interface for dynamic plug ins Section 5 10 2 Kui High level Frama C front end quite deprecated Config Information about Frama C version Plugin General services for plug ins Section 5 6 Cmdline Command line parsing Section 5 12 Log Operations for printing messages Section 5 7 Base Parameters Kernel Parameters Section 5 12 Modules Journal Journalization Section 5 9 CilE Useful Cil extensions Alarms Alarm management Kernel_type Type value for kernel types Section 5 10 2 Stmts_graph Accessibility checks using CFG Visitor Visitor Frama C visitors subsume Cil ones Section 5 14 Pretty Ast_printer Pretty printers for AST node printers Printer Main class for pretty printing Boot Last linked module Section 5 13 Initializer Gui_init Very early initialization of the GUI Section 5 13 Special_hooks Registration of some kernel hooks Figure 6 4 Main kernel modules 80 6 2 CONFIGURE IN e Directory gui contains the gui implementation part common to all plug ins See Section 5 17 for more details 6 2 Configure in Figure 6 5 presents the different parts of configure in in the order that they are introduced in the file The second column of the tabular says whether the given part has to be modified eventually by a kernel integrated plug in developer More details are provided below Id Name Mod Reference 1 Configuration of make no 2 Configuration of OCaml no 3 Configuration of mandatory tool
101. ons that use the kernel and possibly others plug ins through the APIs they register in the Frama C kernel See Section 4 4 for details 29 CHAPTER 4 SOFTWARE ARCHITECTURE Plug ins Standard Plug ins Kernel integrated Plug ins Kernel integrated Plug ins Types Plug in types 1 Plug in types q Figure 4 1 Architecture Design 30 4 2 CIL C INTERMEDIATE LANGUAGE 4 2 Cil C Intermediate Language Cil 17 is a high level representation along with a set of tools that permit easy analysis and source to source transformation of C programs Frama C uses Cil as a library which performs the main steps of the compilation of C programs pre processing lexing parsing typing and linking and outputs an abstract syntax tree AST ready for analysis From the Frama C developer s point of view Cil is a toolbox usable through its APT and providing e the AST description module Cil_types e useful AST operations module Ci1 e some simple but useful miscellaneous datastructures and operations mainly in module Cilutil and e some syntactic analysis like a syntactic call graph computation module Callgraph or generic forward backward dataflow analysis module Dataflow Frama C indeed extends Cil with ACSL ANSI ISO C Specification Language 1 its specifi cation language The extended Cil APT consequently provides types and operations in order to properly deal with annotated C prog
102. ory 6 12 The sre directory e 4 254 228 bea Hage ego ea ea be etal oe Po we eS CONTENTS Makenles ca ce ue pue ne bebe RR GER RES Red dE 82 Gal OVERVIOW ce osaga d ma a Gea tests CNT Teese 82 6 3 2 Sections of Makefile Makefile config in and Makefile common 82 6 3 3 Variables of Makefile dynamic and Makefile plugin 88 O d4 Makefile MAMIE oo t Lu e n sde nan las de da 91 GE TIE Lo be CRS Oe ee Pe Pea hae A oe ere Rue 91 A Changes 95 Bibliography 99 List of Figures 101 Index 103 Very Important Preliminary Warning This document is no longer consistent with the current Frama C implementation Frama C Nitrogen 20111001 When a particular part of the document is known to be out of date the following mention comes in front of it This part is out of date Please report as feature request on http bts frama c com if you really need it But even without this mention any part of the document may be also obsolete feel free to report us such a behavior as feature request on http bts frama c com In any way it is not a bug but an assumed possible behavior Please be sure that we will do our best to improve this awkward situation in future releases Foreword This is the documentation of the Frama C implementation which aims to help developers integrate new plug ins inside this platform It started as a deliverable of the task 2 3 of the ANR RNTL project CAT The content of
103. pendency exists on the system Second it verifies for each plug in that its dependencies are met Section 5 2 4 explains how to make a plugin depend on a given library or tool The present section deals with the first part that is how to check for a given library or tool on a system Configuration of new libraries and configuration of new tools are similar In this section we therefore choose to focus on the configuration of new libraries This is done by calling a predefined macro called configure_library The configure_library macro takes three arguments The first one is the uppercase name of the library the second one is a filename which is used by the script to check the availability of the library In case there are multiple locations possible for the library this argument can be a list of filenames In For tools there is a macro configure_tool which works in the same way as configure_library 37 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT this case the argument must be properly quoted i e enclosed in a pair Each name is checked in turn The first one which corresponds to an existing file is selected If no name in the list corresponds to an existing file the library is considered to be unavailable The last argument is a warning message to display if a configuration problem appears usually because the library does not exist Using these arguments the script checks the availability of the library Results of this
104. r let name postdominator end 5 11 5 Registering a New Internal State Here we explain how to register and use an internal state in Frama C Registration through the use of low level functor Project Computation Register is postponed in Section 5 11 6 because it is more tricky and rarely useful In most non Frama C applications a state is a usually global mutable value One can use it in order to store results of the analysis For example inside Frama C the following piece of code would use value state in order to memoize some information attached to statements open Cilutil type info Kernel function t Cil types varinfo let state info StmtHashtbl t StmtHashtbl create 97 let compute info let memoize s try StmtHashtbl find state s with Not found StmtHashtbl add state s compute info s let run O Db Value compute memoize some stmt However if one puts this code inside Frama C it does not work because this state is not registered as a Frama C internal state A direct consequence is that it is not saved on the disk For this purpose one has to transform the above code into the following one module State Cil computation StmtHashtbl Datatype Couple Kernel function Datatype Cil datatype Varinfo struct let size 97 let name state let dependencies Db Value self end let compute info let memoize State memo compute info let run Db Value compute memoize som
105. r example a prede fined memo function is used in order to memoize the computation of compute_info This memoization function implicitly operates on the hashtable hidden in the internal representation of State Postponed dependencies A plug in p may want to export its state kind in the previous example that is value State self This exportation offers the possibility to other plug ins to depend on this state It is a bit tricky because the state kind has to be accessible through Db There is two ways to achieve such a goal First the internal state has to be compiled before Db usually the internal state has to be somewhere in directory p_types see Section 5 10 1 Actually it is quite difficult because the computation of the internal state may be complex and so should not be in p_types The second way is to put a delayed reference to self i e the state kind in Db thanks to Project Computation dummy which provides a dummy kind This reference is going to be initialized at the plug in initialization time see Section 5 13 Now if another plug in has an internal state which depends on Db My_plugin self it cannot put the dependence when the functor creating the state is applied because the order of plug in initialization is not specified see Section 5 13 for more details about initialization steps So you have to postpone the addi tion of this dependency usually by using the function Cmdline run_after_extending_stage see Section 5 13
106. r its redirection is print on output The routine immediately locks the output of Log and prints the provided message All message echoes are delayed until the routine actually returns Notification to listeners is not delayed however print delayed This variant locks the output only when the first character would be written to output This gives a chance to a message to be echoed before your text is actually written Remark that these two routines can not be recursively invoked since they have a lock to a non delayed output channel This constraint is verified at runtime to avoid incorrect interleaving and you would get a fatal error if the situation occurs Warning these routine are dedicated to expensive output only You get the advantage of not buffering your text before printing But on the other hand if you have messages to be echoed during printing they must be stacked until the end of your printing You get a similar functionality with Parameters CodeOutput output This routine prints your text by calling Log print_ delayed unless the command line option ocode has been set It this case your text is written to the specified file 5 8 Types as first class values Not written yet please report as feature request on http bts frama c com if you really need this section You may also read some articles 19 20 related to this section 5 9 Journalization Not written yet please report as
107. r the Lesser General Public License LGPL and CEA copyright you 5Or whatever your favorite text editor is 23 CHAPTER 2 TUTORIAL simply have to edit the section File headers license policy of Makefile with the following line File Makefile CEA_LGPL src hello ml others files Now executing make headers This adds a header on files of plug in hello in order to indicate that they are under the desired license 24 Chapter 3 Tutorial of the Future Target readers beginners Not written yet please report as feature request on http bts frama c com if you really need this section 3 1 What a Plug in Look Like Not written yet please report as feature request on http bts frama c com if you really need this section 3 2 A Simple Script Not written yet please report as feature request on http bts frama c com if you really need this section 3 3 Registering a Script as a Plug in Not written yet please report as feature request on http bts frama c com if you really need this section 3 4 Displaying Messages Not written yet please report as feature request on http bts frama c com if you really need this section 3 5 Adding Command Line Options Not written yet please report as feature request on really need this section 25 http bts CHAPTER 3 TUTORIAL OF THE FUTURE 3 6 Writing a
108. rams Cil modules belong to directory and subdirectories of cil src 4 3 Kernel On top of the extended Cil API the Frama C kernel groups together specific services providing in different modules which are described below e In addition to the Cil utilities Frama C provides useful operations mainly in module Extlib and datastructures e g specialized version of association tables like Rangemap These modules belong to directories src lib and src misc and they are not specific to the analysis or transformation of C programs e Frama C provides generic lattices useful for abstract interpretation module Abstract_interp and some pre instantiated arithmetic lattices module Ival The abstract interpretation toolbox is available in directory src ai e Frama C also provides different representations of C memory states module Locations and data structures using them e g association tables indexing by memory states in modules Lmap and Lmap_bitwise The memory state toolbox is available in directory src memory_state e Moreover directory src kernel provides a bunch of very helpful operations over the extended Cil AST For example module Globals provides operations dealing with global variables functions and annotations while module Visitor provides inheritable classes in order to permit easy visiting copying or in place modification of the AST Besides Frama C also provides some general purpose services used by all other modul
109. re return result of the analysis end 52 5 10 PLUG IN REGISTRATION AND ACCESS File Makefile UNPACKED_DIRS plugin_types Extend this variable with the new directory This design choice has a side effect it reveals exported types You can always hide them using a module to encapsulate the types and provide corresponding getters and setters to access them At this point part of the plug in code is outside the plug in implementation This code should be linked before Db To this effect the files containing the exterior plug in code must be added to the Makefile variable PLUGIN_TYPES_CMO see Section 6 3 3 5 10 2 Dynamic Registration and Access Target readers standard plug ins developers Registration of kernel integrated plug ins requires to modify module Db which belongs to the Frama C kernel Such a modification is not possible for standard plug ins which are fully independent of Frama C Consequently the Frama C kernel provides another way for registering a plug in through the module Dynamic In short you have to use the function Dynamic register in order to register a value from a dynamic plug in and you have to use function Dynamic get in order to apply a function previously registered with Dynamic register Registering a value The signature of Dynamic register is as follows val register plugin string gt string a Type t a unit The first argument is the name of the plug in reg
110. register the type 7 itself as a datatype using functor Project Datatype Register A datatype is a type that is aware of projects Simi larly to computations module Datatype resp Cil_datatype provides pre defined datatypes and datatypes builder for elaborated Cil types Section 5 11 4 details how to register a new datatype Example 5 18 If you have to register a reference to a boolean initialized to false as an internal state you have to write the following code module My Bool Ref Computation Ref struct include Datatype Bool let default false end struct let dependencies let name My_Bool_Ref end These datastructures are only mutable datastructures like hashtables arrays and references because global states are always mutable TOn the contrary to computations these types are either mutable or persistent because the registration of a type may require the registration of its subtypes in the sense of syntactically contained in 57 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT 5 11 4 Registering a New Datatype In order to register a new datatype you have to apply functor Project Datatype Register which is a quite low level functor In most cases a direct application of this functor is actually not required because some higher level and easier to use functor does it for you We explain here the three different possible situations Simple registration If the datatype to register is not hash consed or doe
111. rence to a function This reference is not initialized in the implementation of Db we use mk_fun declared in the opened module Extlib in order to declare the reference without instantiating it This instantiation has to be done by the plug in itself Otherwise a call to Db run raises the exception Extlib NotYetImplemented In order to fix this we modify the module Register as follows File src hello register ml definition of run let O Db Hello run run It is important to note that the reference Db Hello run is set at the OCaml module initial ization step So the body of each Frama C function can safely dereference it Documentation We have properly documented the interface of Db with ocamldoc through special comments between and This documentation is generated by make doc In par ticular this command also generates an internal documentation for hello which is accessible in the directory doc code hello Hiding the Implementation Finally we hide the implementation of hello to other de velopers in order to enforce the architecture invariant which is that each plug in should be used through Db see Chapter 4 For this purpose we add an empty interface to the plug in in the following way File src hello Hello mli Hello World plug in No function is directly exported they are registered in Db Hello Note the unusual capitalization of the filename Hello mli which is required for compilation purposes Inde
112. riable LICENSES with this variable 3 4 Add a text file in directory headers containing the headers to add into files of your Add a text file in directory licenses containing your licenses plug in those assigned by v The filename must be the same than the variable name v Moreover this file should contain a reference to the file containing the whole license text Run make headers 76 Chapter 6 Reference Manual This chapter is a reference manual for plug in developers It provides details completing Chapter 5 6 1 File Tree This Section introduces the main parts of Frama C in order to quickly find useful information inside sources Our goal is not to introduce the Frama C software architecture that is the purpose of Chapter 4 nor to detail each module that is the purpose of the source documen tation generated by make doc The directory containing the Cil implementation is detailed in Section 6 1 1 while the directory containing the Frama C implementation itself is presented in Section 6 1 2 Figure 6 1 shows all directories useful to plug in developers More details are provided below Kind Name Specification Reference Frama C root directory src Frama C implementation Section 6 1 2 cil Cil source files Section 6 1 1 Sources ocamlgraph OcamlGraph source files external Source of external free libraries Tests tests Frama C test suites Section 5 5 ptests ptests imple
113. ring a New Datatype 58 5 11 5 Registering a New Internal State 59 5 11 6 Direct Use of Low level Functor Project Computation Register 61 a aor ac ee 4 Pe ae Gre oe De ee ES 62 Command Line Options s r sps 240 65 Pee eae Mie au Pa au he 63 Tnvtialigation Steps L 4 34 4 4 ho AGP ee RU ds ma a ha deal es 65 o 200 ia coal Go SUR MOD Bel ao RE NN Wo UNE So as 67 BIAT Enty POMS q acg eie sn alg ee a e ew ee Bk ale ee des 68 DS IM II 68 5 14 3 Action Perlormed s 0 444444 4 448 8444 de eee ab dae das 68 5 14 4 Visitors and Projects 69 5 14 5 In place and Copy Visitors 69 5 14 6 Differences Between the Cil and Frama C Visitors 70 DT Ezample pu Baa a Pee Da Hans Ae RUN UNE PR ae de 70 Lopical ADDOTSUODA sora ee ss st aer date oe PX 71 ia Lim ye LL a eh se ae ARR UNE de PME NS 72 D10 1 Representations cesas aca w ad eee daw da dd ea der 72 5 16 2 Map Indexed by Locations 73 GUIESTEUSION asocia ee ER ew REE EE Re eh eR HAS 73 Documentation o L amp don ee EA Le ee Se eh Be De 73 5 18 1 General Ov rview 4 LL 4 4 rimar au au au eS 74 518 2 Source Documentation 2 4 saca ma aa Le hote ds es 74 Da VWEDSILE u se es Goa ease NO ARENA a Res 75 License PONCY 22 iG eee PDEA ERD ame RARE ame etre Pile Tiss LS LUS a aS eR WOE a eR Pe RES BS 6 1 1 The cil direct
114. rinting sets all the commands to be used for pretty printing Example 6 1 Consider the following target foo in a plug in specific Makefile foo bar PRINT_CP CP lt Executing make foo prints Copying to foo while executing make foo VERBOSEMAKE yes prints cp f bar foo If one of the two commands is missing for the target foo either make foo or make foo VERBOSEMAKE yes will not work as expected Tests defines a generic template for testing plug ins Generic rules contains rules in order to automatically produces different kinds of files e g cm iox from ml or mli for Objective Caml files 85 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 CHAPTER 6 REFERENCE MANUAL Global plug in variables declares some plug in specific variables used throughout the makefile Additional global variables declares some other variables used throughout the make file Main targets provides the main rules of the makefile The most important ones are top byte and opt which respectively build the Frama C interactive bytecode and native toplevels Coverage defines how compile the eponymous library Ocamlgraph defines how compile the eponymous library Frama C Kernel provides variables and rules for the Frama C kernel Each part is described in specific sub sections After Section Kernel ther
115. rld plug in consists of only two files Makefile and hello_world ml 1 Create the two files Makefile and hello_world ml containing the lines given in the frames at the end of this section The name of each compilation unit here hello_world must be different of the plug in name set by the Makefile here Hello in order to compile a plug in 2 Run make to compile it 3 Run make install to install the plug in You need to have write access to the FRAMAC_LIBDIR plugins directory 4 Test your plug in with frama c byte hello The sentence Hello Frama C World is printed File Makefile Example of Makefile for dynamic plugins Frama c should be properly installed with make install before any use of this makefile FRAMAC_SHARE shell frama c byte print path FRAMAC_LIBDIR shell frama c byte print libpath PLUGIN_NAME Hello PLUGIN_CMO hello_world include FRAMAC_SHARE Makefile dynamic File hello _world ml xx The traditional Hello world plugin It contains one boolean state Enabled which can be set by the command line option hello When this option is set it just pretty prints a message on the standard output xx Register the new plug in Hello World and provide access to some plug in dedicated features module Self Plugin Register struct let name Hello world let shortname hello let help The famous Hello world plugin end Re
116. rrent project into file foo sav in a previous Frama C session thanks to the following instruction Project save foo sav In a new Frama C session executing the following lines of code assuming the value analysis has never been computed previously let print computed Format printf b Db Value is computed in print computed x false x 5A session is one execution of Frama C through frama c or frama c gui 55 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT let old Project current in try let foo Project load name foo foo sav in Project set current foo Db Value compute print computed true x Project set current old print computed false with Project IOError _ gt exit 1 displays false true false This example shows that the value analysis has been computed only in project foo and not in project old An alternative to the use of Project set_current is the use of Project on which applies an operation on a given project without changing the current project i e locally switch the current project in order to apply the given operation and after restore the initial context Example 5 16 The following code is equivalent to the one given in Example 5 15 let print computed Format printf b Db Value is computed in print computed x false try let foo Project load name foo foo sav in Project on foo fun O gt Db Value compute pri
117. s al AST nodes cias ve dus Na aa san OE we ea OS 70 6 1 Fraima C directories sa hh a a ee ue ae ee sdb ee 77 6 2 CUCOIECIONES Lead ess BAERS ete SE Vibes 78 603 Kornel directories a e aace de ban ae a Pa he salon nas 79 64 Mam kornel modules s sarsa L a Li peines du due mate 80 GS BEGLOUS Ol configure ns oq s sachos a s agrea Eii hor wa h aa 8 81 6 6 Relationship between the Makefiles 83 6 7 Sections of Makefile config in Makefile common and Makefile 84 6 8 Standard parameters of Makefile dynamic and Makefile plugin 87 6 9 Special parameters of Makefile dynamic and Makefile plugin 89 6 10 Variables defined by Makefile plugin 91 OLI ptests OPONE 5 ua Li Lio Liu Laos Pade Dee male 92 6 12 Directives in configuration headers of test files 93 101 INDEX Abstract Interpretation 72 Lattice see Lattice Toolbox 31 73 79 Type 58 Abstract Syntax Tree see AST Abstract_interp 31 73 79 Lattice 73 ACSL 29 31 36 78 Frontend 79 ai 79 Alarms 80 Annotation 31 68 71 80 Annotations 72 80 add_assert 71 ANSI C Specification language see ACSL Architecture 13 16 29 Plug in 25 AST 29 31 54 56 67 68 71 78 80 Copying 69 70 Initializer 80 Modification 31 35 55 68 70 Sharing see Sharing Ast 80 get 55 self 55 Ast_info 80 Ast_printer 80 bin 78 Binary 78 Boot
118. s echoed in the terminal This echo may be delayed until message completion when once has been used Upon message completion the message is emitted and sent to all globally registered hook functions unless the emitwith option has been used To interact with this general procedure the plug in developer can use the following functions defined in module Log val set echo plugin string kinds kind list bool gt unit val add listener plugin string kinds kind list event unit unit Continuations The logging routines take as argument a polymorphic formatting string followed by the formatting parameters and finally return unit It is also possible to catch the generated message and to pass it to a continuation that finally returns a value different than unit For this purpose you must use the with_ lt log gt routines variants These routines take a continuation f for additional parameter After emitting the corresponding message in the normal way the message is passed to the continuation f Hence f has type event gt a and the log routine returns a For instance you typically use the following code fragment to return a degenerated value while emitting a warning let ee faci n if n gt 12 then with warning fun 0 Overflow for d return 0 instead x else if n lt i then 1 else n fact n 1 Generic Routines The Log Messages interface provides two generic routines that can be used instead o
119. s libraries no 4 Configuration of non mandatory tools libraries no 5 Platform configuration no 6 Wished Frama C plug in yes Sections 5 2 2 and 5 2 4 7 Configuration of plug in tools libraries yes Section 5 2 3 8 Checking plug in dependencies yes Section 5 2 5 9 Makefile creation yes Section 5 2 2 10 Summary yes Section 5 2 2 Figure 6 5 Sections of configure in 1 Configuration of make checks whether the version of make is correct Some useful option is enable verbosemake resp disable verbosemake which set resp unset the verbose mode for make In verbose mode full make commands are displayed on the user console it is useful for debugging the makefile In non verbose mode only command shortcuts are displayed for user readability 2 Configuration of OCaml checks whether the version of OCaml is correct 3 Configuration of other mandatory tools libraries checks whether all the external mandatory tools and libraries required by the Frama C kernel are present 4 Configuration of other non mandatory tools libraries checks which external non mandatory tools and libraries used by the Frama C kernel are present 5 Platform Configuration sets the necessary platform characteristics operating sys tem specific features of gcc etc for compiling Frama C 6 Wished Frama C Plug ins sets which Frama C plug ins the user wants to compile 7 Configuration of plug in tools libraries checks the availability of e
120. s not contain hash consed ones i e it is not itself hash consed or composed of Cil_types fundec or any Frama C abstract interpretation type the easiest way of registering a new datatype d is to apply one of functors Persistent or Imperative of module Project Datatype depending on the nature of d whether it is persistent The only difference between both functors is that you have to provide a copy function for imperative i e mutable datatypes This copy function is only used by Project copy Example 5 19 For registering a type t containing an immutable field a just do type a da int Project Datatype Persistent struct type t a let name a end If the field a is mutable just write type a mutable a int Project Datatype Imperative struct type t let copy let name end a x a nan iw v Using predefined datatypes or datatype builders For most useful types the corre sponding datatypes are already provided in modules Datatype e g Datatype Int for type int and Cil_datatype e g Cil_datatype Stmt for type Cil_types stmt Moreover both modules provides a bunch of functors which help to build complex datatypes when Project Datatype Persistent and Project Datatype Imperative cannot be used Inter faces of modules Datatype and Cil_datatype provided all the available modules Example 5 20 For registering the type of an hashtable associating varinfo to list of kernel functions it is not possible to
121. signature Abstract_interp Lattice For this purpose functors of the abstract interpretation tool box can help see in particular module Abstract_interp 5 17 GUI Extension Prerequisite knowledge of Lablgtk2 Each plug in can extend the Frama C graphical user interface aka GUI in order to support its own functionalities in the Frama C viewer For this purpose a plug in developer has to register a function of type Design main_window_extension_points unit thanks to Design register_extension The input value of type Design main_window_extension_points is an object corresponding to the main win dow of the Frama C GUI It provides accesses to the main widgets of the Frama C GUI and to several plug in extension points The documentation of the class type Design main_window_extension_points is accessible through the source documentation see Section 5 18 The GUI plug in code has to be put in separate files into the plug in directory Furthermore in the Makefile the variable PLUGIN_GUI_CMO has to be set in order to compile the GUI plug in code see Section 6 3 3 Besides time consuming computations have to call the function Db progress from time to time in order to keep the GUI reactive The GUI implementation uses Lablgtk2 12 you can use any Lablgtk2 compatible code in your gui extension A complete example of a GUI extension may be found in the plug in Occurrence see file src occurrence register_gui ml Potential issues
122. t respectively correspond to the bytecode and native versions of bina ries If you wish and before having fun with Frama C you can e test the compiled platform with make tests e generate the source documentation with make doc e generate navigation tags for emacs with make tags 2 2 2 Plug in Integration Overview Figure 2 2 shows how a kernel integrated plug in may integrate in the Frama C platform Some elements of this figure are pragmatically explained in the remaining sections of this tutorial The implementation of the plug in is provided inside a specific directory and is connected to the Frama C platform thanks to some registration points These registrations are performed either through hooks by applying a function or a functor or directly by modifying some specific part of Frama C files That is the very major difference with integrating standard plug ins standard plug ins never modify Frama C files For instance you have to extend Db with your plug in specific operations and to register them inside it if you want people to be able to use your plug in see Section 2 2 5 However most of the registration for instance extending the Frama C entry point works the same as for standard plug ins see Section 2 1 You also have to modify the files Makefile and configure in in order to properly link your plug in with Frama C see Section 2 2 4 Moreover the developer may provide a plug in interface which should usually be empty
123. the Frama C visitor should occur There are a few differences between the two the Frama C visitor inherits from the Cil one These differences are summarized in Section 5 14 6 which the reader already familiar with Cil is invited to read carefully 5 14 1 Entry Points Cil offers various entry points for the visitor They are functions called Cil visitCilAstType where astType is a node type in the Cil s AST Such a function takes as argument an in stance of a cilVisitor and an astType and gives back an astType transformed according to the visitor The entry points for visiting a whole Cil_types file Cil visitCilFileCopy Cil visitCilFile and visitCilFileSameGlobals are slightly different and do not support all kinds of visitors See the documentation attached to them in cil mli for more details 5 14 2 Methods As said above there is a method for each type in the Cil AST including for logic annotation For a given type astType the method is called vastType and has type astType astType visitAction where astType is either astType or ast Type list for instance one can transform a global into several ones visitAction describes what should be done for the children of the resulting AST node and is presented in the next section In addition some types have two modes of visit one for the declaration and one for use This is the case for varinfo vvdec and vvrbl logic_var vlogic_var_decl and vlogic_var_use logic_info vl
124. the current table but in the table of the new project To avoid the cost of switching projects back and forth all operations on the new project are queued until the end of the visit as mentioned above This is done in the following statement Queue add fun gt Annotations add_ assert x the following line is incorrect since the new kernel function is not yet created x Kernel function find englobing kf stmt stmt Ast self assertion self get filling actions DoChildren _ DoChildren end x This function returns a new project initialized with the current file plus the annotations related to division let create syntactic check project File create project from visitor syntactic check new non zero divisor let create syntactic check project 5 15 Logical Annotations Prerequisite Nothing special apart of core OCaml programming Logical annotations set by the users in the analyzed C program are part of the AST However others annotations those generated by plug ins are not directly in the AST because it would contradict the rule an AST must never be modified inside a project see Section 5 11 2 So all the logical annotations including those set by the users are put in projectified states Anytime a plug in wants either to access to an annotation or to add a new one or to modify 71 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT an existing one it must use these states and not
125. tion 5 2 5 Finally Section 5 2 3 presents the configuration of external libraries and tools needed by a new plug in but not used anywhere else in Frama C 5 2 1 Principle When you execute autoconf file configure in is used to generate the configure script Each Frama C user executes this script to check his system and determine the most appropriate configuration at the end of this configuration if successful the script summarizes the status of each plug in which can be e available everything is fine with this plug in e partially available either an optional dependency of the plug in is not fully available or a mandatory dependency of the plug in is only partially available or e not available either the plug in itself is not provided by default or a mandatory de pendency of the plug in is not available The important notion in the above definitions is dependency A dependency of a plug in p is either an external library tool or another Frama C plug in It is either mandatory or optional A mandatory dependency must be present in order to build p whereas an optional dependency provides features to p that are additional but not highly required especially p must be compilable without any optional dependency Hence for the plug in developer the main role of configure in is to define the optional and mandatory dependencies of each plug in Another standard job of configure in is the addition of options enable p and disable
126. two flavors inplace_visit and copy_visit In the in place mode nodes are visited in place while in the copy mode nodes are copied and the visit is done on the copy For the nodes shared across the AST varinfo compinfo enuminfo typeinfo stmt logic_var logic_info and fieldinfo sharing is of course preserved and the mapping between the old nodes and their copy can be manipulated explicitly through the following functions e reset_behavior_name resets the mapping corresponding to the type name e get_original_name gets the original value corresponding to a copy and behaves as the identity if the given value is not known e get_name gets the copy corresponding to an old value If the given value is not known it behaves as the identity e set_name sets a copy for a given value Be sure to use it before any occurrence of the old value has been copied or sharing will be lost 69 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT get_original_name functions allow to retrieve additional information tied to the original AST nodes Its result must not be modified in place this would defeat the purpose of operating on a copy to leave the original AST untouched Moreover note that whenever the index used for name is modified in the copy the internal state of the visitor behavior must be updated accordingly via the set_name function for get_original_name to give correct results The list of such indices is given Figure 5 2
127. ue for each plug in p Makefile plugin provides some variables which may be used after its inclusion defining p These variables are listed in Figure 6 10 For each variable of the form p_VAR its behavior is exactly equivalent to the value of the parameter PLUGIN_VAR for the plug in p Variables of the form p_ CMX have no PLUGIN_ CMX counterpart but their meanings should be easy to understand plugin is the module name of the considered plug in i e as set by PLUGIN_NAME 90 6 4 TESTING Kind Name Usual information plugin_DIR plugin_CMO plugin_CMI Source files plugin_CMX plugin_TYPES_CMO plugin_TYPES_CMX plugin_BFLAGS plugin_OFLAGS plugin _LINK_BFLAGS plugin_LINK_OFLAGS plugin_LINK_GUI_BFLAGS plugin_LINK_GUI_OFLAGS plugin_DEPFLAGS Compilation flags Dependencies plugin_GENERATED plugin_DOCFLAGS Documentation plugin_TYPES_TODOC lugin_TESTS_DIRS Testing re J plugin_TESTS_LIB Figure 6 10 Variables defined by Makefile plugin 6 3 4 Makefile dynamic Not written yet please report as feature request on http bts frama c com if you really need this section 6 4 Testing Section 5 5 explains how to test a plug in Here Figure 6 11 details the options of ptests while Figure 6 12 shows all the directives that can be used in the configuration header of a test or a test suite Some details about them are provided below The commands provided through the d
128. ug in will be dynamically linked within the Frama C kernel The plugin name must contain only alphanumeric characters and underscores It must be the same as the name value given as argument to the functor Plugin Register of section 5 6 with spaces replaced by underscore The macro check_ plugin sets the following variables FORCE_OCCURRENCE REQUIRE_OCCURRENCE USE_OCCURRENCE ENABLE_OCCURRENCE and DYNAMIC_OCCURRENCE The first variable indicates if the user explicitly requires the availability of occurrence via setting the option enable occurrence The second and third variables are used by oth ers plug ins in order to handle their dependencies see Section 5 2 5 The fourth variable ENABLE_OCCURRENCE indicates the plug in status available partially available or not avail able If enable occurrence is set then ENABLE_OCCURRENCE is yes plug in available if disable occurrence is set then its value is no plug in not available If no option is specified on the command line of configure its value is set to the default one according to the value of the fourth argument of check_plugin Finally DYNAMIC_OCCURRENCE indicates whether the plug in will be dynamically linked within the Frama C kernel 5 2 3 Configuration of New Libraries or Tools Some plugins needs additional tools or libraries to be fully functional The configure script takes care of these in two steps First it checks that an appropriate version of the external de
129. ult value is tests notdir PLUGIN_DIR e Variable PLUGIN_TESTS_LIB is the cmo plug in specific files used by plug in tests Do not write its file path which is PLUGIN_TESTS_DIRS nor its file extension which is cmo e Variable PLUGIN_NO_DEFAULT_TEST indicates whether the test directory of the plug in should be considered when running Frama C default test suite When set to a non empty value the plug in tests are run only through make PLUGIN_NAME _tests e Variable PLUGIN_INTERNAL_TEST indicates whether the tests of the plug in are included in Frama C s own tests directory When set to a non empty value the tests are searched there When unset tests are assumed to be in the tests directory of the plugin main directory itself Having the tests of a plugin inside Frama C s own tests suite is dep recated Plugins should be self contained e Variable PLUGIN_DISTRIB_BIN indicates whether the plug in should be included in a binary distribution e Variable PLUGIN_DISTRIBUTED indicates whether the plug in should be included in a source distribution e Variable PLUGIN_DISTRIB_EXTERNAL is the list of files that should be included within the source distribution for this plug in They will be put at their proper place for a release As previously said the above variables are set before including Makefile plugin in order to customize its behavior They must not be use anywhere else in the Makefile In order to deal with this iss
130. urce no raoi PLUGIN_ENABLE Whether the plug in has to be com no piled PLUGIN_DYNAMIC Whether the plug in is dynamically no linked with Frama C PLUGIN_HAS_MLI Whether the plug in gets an interface PLUGIN_CMO cmo plug in files Source files PLUGIN_CMI cmi plug in files without correspond ing cmo PLUGIN_TYPES_CMO cmo plug in files not belonging to PLUGIN_DIR PLUGIN_GUI_CMO cmo plug in files not belonging to PLUGIN_DIR PLUGIN_BFLAGS Plug in specific flags for ocamlc PLUGIN_OFLAGS Plug in specific flags for ocamlopt Compilation PLUGIN_EXTRA_BYTE Additional bytecode files to link flags against PLUGIN_EXTRA_OPT Additional native files to link against PLUGIN_LINK_BFLAGS Plug in specific flags for linking with ocamlc PLUGIN_LINK_OFLAGS Plug in specific flags for linking with ocamlopt PLUGIN_LINK_GUI_BFLAGS Plug in specific flags for linking a GUI with ocamlc PLUGIN_LINK_GUI_OFLAGS Plug in specific flags for linking a GUI with ocamlopt Figure 6 8 Standard parameters of Makefile dynamic and Makefile plugin 87 CHAPTER 6 REFERENCE MANUAL 6 3 3 Variables of Makefile dynamic and Makefile plugin Figures 6 8 and 6 9 presents all the variables that can be set before including Makefile plugin or Makefile dynamic see Sections 5 3 and 5 4 The last column is set to no if and only if the line is not relevant for a standard plug in developer Details are provided below e Variable PLUGIN_NAME is the
131. ure If you have an Objective Caml version lt 3 11 then only bytecode plug ins are available Upgrade to Objective Caml gt 3 11 if you need native code plug ins 13 CHAPTER 2 TUTORIAL Plug in directory Caption part not covered in this chapter tutorial registration points Figure 2 1 Plug in Integration Overview The implementation of the plug in is provided inside a specific directory The plug in registers with the Frama C platform through kernel provided registration points These registrations are performed through hooks by applying a function or a functor For instance the next section shows how to e extend the Frama C entry point thanks to the function Db Main extend if you want to run plug in specific code whenever Frama C is executed e use specific plug in services provided by the module Plugin such as adding a new Frama C option 2 1 2 Hello Frama C World A very basic plug in is the Hello World plug in This plug in adds a command line option hello to Frama C and pretty prints the message Hello World whenever the option is set It is possible to program such an option just with the module Arg provided by the Objective Caml standard library and without the addition of a Frama C plug in but we use this example to introduce the bases of plug in development This plug in is our running example in this chapter 14 2 1 STANDARD PLUG IN The Hello Wo
132. used as a state you have to use it Actually in the Frama C kernel there is no direct use of this functor This functor takes three arguments The first and the third ones respectively correspond to the datatype and to information name and dependencies of the internal states they are similar to the corresponding arguments of the high level functors see Section 5 11 5 The second argument explains how to handle the local version of the value of the internal state under registration Indeed here is the key point from the outside only this local version is used for efficiency purpose It would work if projects do not exist Each project knows a global version the set of these global versions is the so called internal states The project management system automatically switches the local version when the current project changes in order to conserve a physical equality between local version and current global version So for this purpose the second argument provides a type t type of values of the state and five functions create creation of a new fresh state clear cleaning a state get getting a 61 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT state set setting a state and clear_if_project how to clear each value of type project in the state if any The following invariants must hold create returns a fresh value 5 1 Vp of type t create clear p set p get 5 2 Vp of type t copy p returns a fresh v
133. 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 5 6 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 Objective Caml standard libraries For instance you should never use Pervasives stdout and Pervasives stderr channels nor Format printf like routines Instead you should use Format fprintf to implement pretty printers for your own complex data and only the printf like routines of Log Messages to display messages to the user All these routines are immediately available from your plug in general services Example 5 10 A minimal example of a plug in using the logging services module Self Plugin Register struct let name foo plugin let shortname foo let descr illustration of logging services end let pp_dg out n Format fprintf out you have at least debug d n let run Self result Hello this is Foo Logs Self debug level 0 Try higher debug levels a pp dg 0 Self debug level 1 If you read this a pp dg 1 Self d
134. w 82 6 3 MAKEFILES Caption ml gt m2 Makefile m1 is included into Makefile m2 ml m2 Makefile m2 is generated from Makefile m1 Plug in Makefiles Generated Makefiles Other kernel Makefiles Figure 6 6 Relationship between the Makefiles 83 CHAPTER 6 REFERENCE MANUAL Name File Mod Reference 1 Working directories Makefile config in no 2 Installation paths Makefile config in no 3 Ocaml stuff Makefile config in no 4 Libraries Makefile config in no 5 Miscellaneous commands Makefile config in no 6 Miscellaneous variables Makefile config in no 7 Variables for plug ins Makefile config in no bis Working directories Makefile common no r 8 Flags Makefile common no 9 Verbosing Makefile common no 10 Shell commands Makefile common no 11 Command pretty printing Makefile common no 12 Tests Makefile common no 13 Generic rules Makefile common no 14 Global plug in variables Makefile no 15 Additional global variables Makefile no 16 Main targets Makefile no 17 Coverage Makefile no 18 Ocamlgraph Makefile no 19 Frama C Kernel Makefile no 20 Plug in sections Makefile yes Section 5 3 21 Generic variables Makefile no 22 Toplevel Makefile no 23 GUI Makefile no 24 Standalone obfuscator Makefile no 25 Tests Makefile no 26 Emacs tags Makefile no 27 Documentation Makefile no 28 Installation Makefile yes Not written yet 29 File headers license policy Makefile yes Section 5 19 30 Makefile rebuild
135. xample there are signatures Plugin INT and Plugin BOOL for integer and boolean parameters Mostly these signatures provide getters and setters for parameters 63 CHAPTER 5 ADVANCED PLUG IN DEVELOPMENT Implementing such an interface is very easy thanks to internal functors provided by the output module of Plugin Register Indeed you have just to choose the right functor according to your option type and eventually the wished default value Below is a list of most useful functors see the signature Plugin General_services for an exhaustive list 1 False resp True builds a boolean option initialized to false resp true 2 Int resp Zero builds an integer option initialized to a specified value resp to 0 3 String resp EmptyString EmptyString builds a string option initialized to a specified value resp to the empty string 4 IndexedVal builds an option for any datatype 7 as soon as you provides a partial function from strings to value of type 7 Each functor takes as argument at least the name of the command line option corresponding to the parameter and a short description for this option Example 5 26 The parameter corresponding to the option occurrence of the plug in occurrence is the module Print defined in the file src occurrence options ml It is implemented as follow module Print False struct let option name occurrence let descr print results of occurrence analysis end So
136. xternal tools and libraries required by plug ins for compilation and execution 8 Checking Plug in Dependencies sets which plug ins have to be disabled at least partially because they depend on others plug ins which are not available at least partially From the outside the GUI may be seen as a plug in with some exceptions 81 CHAPTER 6 REFERENCE MANUAL 9 Makefile Creation creates Makefile from Makefile including information provided by this configuration 10 Summary displays summary of each plug in availability 6 3 Makefiles In this section we detail the organization of the different Makefiles existing in Frama C First Section 6 3 1 presents a general overview Next Section 6 3 2 details the different sections of Makefile config in Makefile common and Makefile Next Section 6 3 3 introduces the variables customizing Makefile plugin and Makefile dynamic Finally Section 6 3 4 shows specific details of Makefile dynamic 6 3 1 Overview Frama C uses different Makefiles plus the plug in specific ones They are e Makefile the general Makefile of Frama C e Makefile config in the Makefile configuring some general variables especially the ones coming from configure e Makefile common the Makefile providing some other general variables and general rules e Makefile plugin the Makefile introducing specific stuff for plug in compilation e Makefile dynamic the Makefile usable by plug in specific Make
137. y_point all the results of analyses depending of it like the value analysis are automatically reset If such a reset was not performed the results of the value analysis would be not consistent with the current entry point Example 5 17 Suppose that the value analysis has previously been computed Format printf b Db Value is computed true x Globals set entry points f true Format printf b Db Value is computed false x As the value analysis has been reset by setting the entry point the above code outputs true false Internal State Registration Overview For registering a new internal state functor Project Computation Register is provided Actually it is quite a low level functor Higher level functors are provided to the developer by modules Computation and Cil_computation that register internal states in a simpler way They internally apply the low level functor in a proper way Module Computation provides internal state builders for standard OCaml datastructures like hashtables whereas Cil_computation does the same for standard Cil datastructures like hashtables indexed by AST statements Registering a new internal state must be performed before parsing com mand line option For this purpose you can register your function through Cmdline run_after_extending_stage see Section 5 13 Section 5 11 5 details how to register a new computation The registration of a data of type 7 requires to
138. ype and use it through the function provided by the plug in APT See Section 5 10 for details 33 Chapter 5 Advanced Plug in Development This chapter details how to use services provided by Frama C in order to be fully operational with the development of plug ins Each section describes technical points a developer should be aware of Otherwise one could find oneself in one or more of the following situations from bad to worse 1 reinventing the Frama C wheel 2 being unable to do some specific things e g saving results of your analysis on disk see Section 5 11 3 3 introducing bugs in your code 4 introducing bugs in other plug ins using your code 5 breaking the kernel consistency and so potentially breaking all the Frama C plug ins e g if you modify the AST without changing project see Section 5 11 2 In this chapter we suppose that the reader is able to write a minimal plug in like hello described in chapter 2 and knows about the software architecture of Frama C chapter 4 Moreover plug in development requires the use of advanced features of OCaml module system classes and objects etc Static plug in development requires some knowledge of autoconf and make Each section summarizes its own prerequisites at its beginning if any Note that the following subsections can be read in no particular order their contents are indeed quite independent from one another even if there are references from on

Plug-In development guide

Contents

Download Pdf Manuals

Related Search

Related Contents