User Manual - Frama-C
Contents
1. 25 CHAPTER 6 ANALYSIS OPTIONS The option no overflow should only be activated when it is guaranteed that the sizes of integer types do not change the concrete semantics of the analyzed code Beware voluntary overflows that are a deliberate part of the implemented algorithm are easy enough to recognize and to trust during a code review Unwanted overflows on the other hand are rather difficult to spot using a code review T he next example illustrates this difficulty Consider the function abs that computes the absolute value of its int argument int abs int x 4 Nee return x 3 With the no overflow option the result of this function is a positive integer for what ever integer passed to it as an argument This property is not true for a conventional ar chitecture where abs MININT overflows and returns MININT Without the no overflow option on the other hand the value analysis detects that the value returned by this function abs may not be a positive integer if MININT is among the arguments The option no overflow may be modified or suppressed in a later version of the plug in unsafe arrays is useful when the source code manipulates arrays within structures It assumes that accesses in the array are always within the correct bounds No warnings are then emitted about possible out of bounds The opposite option called safe arrays is set by default unspecified access may be used to check2. of the analyses provided by Frama C require comparatively little intervention from the user and the collaborative approach proposed in Frama C allows the user to get some impressive results 2 2 1 Frama C as a Lightweight Semantic Extractor Tool Frama C analyzers may be useful for better understanding a C program by extracting semantic information from its code The C language has been in use for a long time and numerous programs today make use of C routines This ubiquity is due to historical reasons and to the fact that C is well adapted for a significant number of applications e g embedded code However the C language exposes many notoriously awkward constructs Many Frama C plug ins are able to reveal what the analyzed C code actually does Equipped with Frama C you can for instance e observe sets of possible values for the variables of the program at each point of the execution e slice the original program into simplified ones e navigate the dataflow of the program from definition to use or from use to definition 2 2 2 Frama C for Formal Verification of Critical Software Frama C allows to verify that source code complies with provided formal specifications Specifications can be written in a dedicated language ACSL ANSI ISO C Specification Lan guage 2 The specifications can be partial concentrating on one aspect of the analyzed program at a time The most structured sections of your existing design documen
3. 1 0 RI 1 0 R2 E return 1 0 1 0 R1 1 0 R2 return retres Hp ragma JessieFloatModel strict int main void int main void it ible R i etres retres O return __retres Function main Statement 2 line 13 in f2 c Variable R has type double It is a local variable It is referenced and its address is not taken Before statement RE 66 6666666667 Figure 8 7 Viewing the analysis results Splash a kernel error source file example c does not exist Figure 8 8 An Error Window 38 Chapter 9 Reporting Errors 9 1 Using the BTS Sometimes Frama C crashes or behaves abnormally so users are invited to file an error report on the Frama C Bugs Tracking System BTS located at http bts frama c com Bug reports can be marked as public or private Public bug reports can be read by anyone and they may be indexed by search engines Private bug reports are shown only to Frama C developers Note however that reporting any category of bug requires having created a BT S account After selecting the adequate project your browser displays the page shown Figure 9 1 This page has also a link to an advanced bugs reporting page that allows to write a more detailed report The different fields of these forms shall be filled in English as precisely as possible in order for the maintenance team to understand and track the problem down easily Below are some recommendations for
4. help Furthermore the option help lists all available plug ins 3 3 2 Frama C Version The current version of the Frama C kernel can be obtained with the option version This option also prints the different paths where Frama C searches objects when required 3 3 3 Verbosity and Debugging Levels The Frama C kernel and plug ins usually output messages either in the GUI or in the console Their levels of verbosity may be set by using the option verbose lt level gt By default this level is 1 Setting 1t to O limits the output to warnings and error messages while setting 1t to a number greater than 1 displays additional informative message progress of the analyses etc In the same fashion debugging messages may be printed by using the option debug lt level gt By default this level is 0 no debugging message is printed By contrast with standard messages debugging messages may refer to the internals of the analyzer and may not be understandable by non developers The option quiet is a shortcut for verbose O debug 0 In the same way that verbose resp debug sets the level of verbosity resp debugging the options kernel verbose resp kernel debug and lt plug in name gt verbose resp lt plug in name gt debug set the level of verbosity resp debugging of the kernel and par ticular plug ins While both the global level of verbosity resp debugging and a specific one are modified the specific one applie
5. lri fr On Windows OS the usual extension exe is added to each file name SFor a single analysis project Multiple projects can only be handled in the interactive version or program matically see Section 7 1 16 3 3 FRAMA C COMMAND LINE AND GENERAL OPTIONS interactively the command frama c gui val foo c can be used to launch the value analysis on the file foo c and starts displaying the results immediately in the GUI Any option requiring an argument may use the following format option name value If the option s argument is a string that is neither an integer nor a float etc the following format is also possible option name value This last format must be used when value starts with a minus sign Most parameterless options have an opposite option often written by prefixing the option name with no For instance the option unicode for using the Unicode character set in messages has an opposite option no unicode for limiting the messages to ACSII Plug ins options with a name of the form lt plug in name gt lt option name gt have their opposite option named lt plug in name gt no lt option name gt For instance the opposite of option ltl acceptance is 1t1 no acceptance 3 3 1 Getting Help The options of the Frama C kernel i e those which are not specific to any plug in can be printed out through the option kernel help The options of a plug in are displayed by using the option lt plug in name gt
6. 1 The BTS Bugs Reporting Page 40 9 2 EXIT STATUS Steps to reproduce provide everything necessary for a maintainer to reproduce the bug input files commands used sequence of actions etc If the bug appears through the Frama C GUI it may be useful to attach the generated journal see Section 7 3 Beware that this journal does not replace nor contain the input files that must be added to the bug report too see below Additional Information any extra information that might help the maintainer Industrial set it to true if you have a maintenance contract with the Frama C development team Upload File click on the Browse button to select a file for uploading Typically this is an archive that contains all files necessary for reproducing your problem It can include source files shell scripts to run Frama C with your options and environment a Frama C journal etc Please check the size of the archive in order to to keep it manageable leave out any object code or executable files that can be easily rebuilt automatically by a shell script for instance View Status set it to private if your bug should not be visible by others users Only yourself and the Frama C developers will be able to see your bug report Report Stay tick if this report shall remain open for further additions After submitting the report you will be notified by e mail about its progress and enter inter active mode on the BTS if necessary
7. Bibliography 45 Index A 7 Foreword This is the user manual of Frama C The content of this document corresponds to the ver sion Beryllium 20090902 dev November 30 2009 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 Micka l Delahaye Philippe Hermann and Benjamin Monate http frama c cea fr Chapter 1 Introduction This is Frama C s user manual Frama C is an open source platform dedicated to the static analysis of source code written in the C programming language The Frama C platform gathers several static analysis techniques into a single collaborative framework This manual gives an overview of Frama C for newcomers and serves as a reference for ex perimented users It only describes those platform features that are common to all analyzers Thus it does not cover use of the analyzers provided in the Frama C distribution Value Anal ysis Slicing Each of these analyses has its own specific documentation 3 Furthermore the development of new analyzers is described in the Plug in Development Guide 4 1 1 Organization of the Document The remainder of this manual is organized in several chapters Chapter 2 provides a general overview of the platform Chapter 3 describes the basic elements for starting the tool in terms
8. Frama C configuration to fail Internal dynamic plug ins may be linked statically This is achieved by passing configure the option with lt plug in name gt static It is also possible to force all dynamic plug ins to be linked statically with the option with all static 19 CHAPTER 4 WORKING WITH PLUG INS 4 3 Installing External Plug ins For installing an external plug in Frama C must be properly installed first In particular frama c print share path must return the share directory of Frama C see Section 3 4 while frama c print lib path must return the directory where the file objects of the Frama C kernel are installed This last directory is automatically chosen when installing Frama C and may be changed by setting the environment variable FRAMAC_LIB The standard way for installing an external plug in from source is to run the sequence of commands make amp amp make install possibly preceded by configure Please refer to each plug in s documentation for installation instructions External plug ins are always dynamic plug ins by default On systems where native dynamic linking is not supported a new executable called frama c lt plug in name gt is automatically generated when an external plug in is compiled This executable contains the Frama C kernel all the static plug ins previously installed and the external plug in On systems where native dynamic linking is available this executable is not nece
9. Frama C knows that it is not necessary to redo the value analysis since the parameters have not been changed Consider now the two following commands frama c save foo sav ulevel 5 unsafe arrays val foo c frama c load foo sav safe arrays 28 7 3 JOURNALISATION The first commands produces the very same result than above However when loading Frama C knows that one parameter changed Thus it discards the saved results of the value analysis and recomputed it on the same source code by using the parameter ulevel 5 safe arrays and the default value of each other parameter In the same way results of one analysis A may depend on results of another one Aa So whenever results of Ag change Frama C automatically discards results of A For instance slicing results depend on value analysis results Thus the slicing results are discarded whenever the value analysis ones are 7 3 Journalisation Journalisation logs each operation that modifies some parameters or results into a file called a journal Observational operations like viewing the set of possibles values of a variable in the GUI are not logged By default the name of the journal is frama c journal ml but it can be modified by using the option journal nane A journal is a valid Frama C dynamic plug in Thus it can be loaded by using the option load script see Section 4 4 The journal replays the very same results than the ones computed in the origina
10. also possible to use the patterns 1 and 2 in the command as place holders for the input files and the output file respectively Here are some examples for using this option frama c cpp command gcc C E I x c filel src file2 i frama c cpp command gcc C E I o 2 1 filel c file2 i frama c cpp command cp 1 2 filel c file2 i frama c cpp command cat 1 gt 2 filel c file2 i frama c cpp command CL exe C E 1 gt 2 filel c file2 i YN Y A SH Additionally the option cpp extra args allows the user to extend the pre processing com mand By default ACSL annotations are not pre processed Pre processing them requires to use gcc as pre processor and to put the option pp annot on the Frama C command line 5 2 Merging the Source Code files After pre processing Frama C parses type checks and links the source code It also performs these operations for the ACSL annotations optionally present in the program Together these steps form the merging phase of the creation of an analysis project 21 CHAPTER 5 PREPARING THE SOURCES Frama C aborts whenever any error occurs during one of these steps However users can use the option continue annot error in order to continue after emiting a warning when an ACSL annotation fails to type check 5 3 Normalizing the Source Code After merging the project files Frama C performs a number of local code transformations in the normali
11. ce ee a a nase 4 Working with Plug ins dl The Plugin a oe e e ad areas nr genauer FS 4 2 Installing Internal Plug ins 4 3 Installing External Plug ins AA Using POCO co psc sia a na DRE RR EG eS HS CONTENTS Preparing the Sources 21 9 1 Pre processing the Source Files 2 2 2 Lo m mn nn 21 9 2 Merging the Source Code files 2 0 0 0 2 21 5 3 Normalizing the Source Code nn nn 22 9 4 Testing the Source Code Preparation e 22 6 Analysis Options 25 Dll PP aa AAA 20 E Le AMD scsi eR RSE REE Rew ER EE RS OH 25 7 General Kernel Services 27 fal WOO oa oe ee eee ewe eee RA 27 Ll AM CM bce ke eee ee Ee eee ee ETE HH 21 Pla MM Pre ea ee en a ee a en Sew HSS 27 7 1 3 Saving and Loading Projects 2565 ies ee eve she ve ee 28 7 2 Dependencies between Analyses o oo a a a a a e a a a 28 fe dn a Wks ou RRR we eraras ERE RE RE EEE Kee 29 8 The Graphical User Interface 31 8 1 The Frama C Main Window 000 ce eee eae 31 SB Mam Functions ocres be eka BRR EM SM EM EA 32 Sal The Memu Bar 4 000 00 0 00 ne a da a AA a 32 8 2 2 The Shortcut Buttons oaoa aa Eh a a des be 35 823 The Contextual Meda 39 Be o css ake oe ae EEB Eee ERE RO GEO A E 39 8 4 Error Windows lt 6 4224446468686 5h 44h 4 ew DCD eee HOES 36 9 Reporting Errors 39 Bl Loma ibe DIS Ge ee ane EERE REDE OOK ESS 39 0 PAOLO sas sssrds di kee ek bw REE Ew AA Al A Changes 43
12. interface is called to create from scratch a new project and fill it with source files see Section 8 2 1 or e a source code transforming analysis has been made The analyzer then creates a new project based on the original project and containing the modified source code typical example is code slicing which tries to simplify a program by preserving a specified behaviour 7 1 2 Using Projects The list of existing projects of a given session is visible in the graphical mode through the Change Project menu see Section 8 2 1 This menu allows the user to switch between different projects during the same session In the batch mode it is not possible to handle a multi project session there is no way to switch from one project to another one through the command line 2T CHAPTER 7 GENERAL KERNEL SERVICES 7 1 3 Saving and Loading Projects A session can be saved to disk and reloaded by using the options save lt file gt and load lt file gt respectively Saving is performed when Frama C exits without error T he same oper ations are available in the GUI through the File Menu see Section 8 2 1 In this case saving is done when clicking on Save or Save as When saving all existing projects are dumped into an unique non human readable file When loading the following actions are done in sequence 1 all the existing projects of the current session are deleted 2 all the projects stored in the file
13. not deal with the development of new plug ins see the Plug in Development Guide 4 It does not deal with usage of plug ins which is the purpose of individual plug in manuals 4 1 The Plug in Taxonomy It is possible to distinguish 2 x 2 kinds of plug ins internal vs external plug ins and static vs dynamic plug ins These different kinds are explained below internal vs external Internal plug ins are those distributed within the Frama C kernel while external plug ins are those distributed independently of the Frama C kernel They only differ in the way they are installed see Sections 4 2 and 4 3 static vs dynamic Static plug ins are statically linked into a Frama C executable see Sec tion 3 2 while dynamic plug ins are loaded by an executable when it is run Despite only being available on some environments see Section 3 1 dynamic plug ins are more flexible as explained in Section 4 4 4 2 Installing Internal Plug ins Internal plug ins are automatically installed with the Frama C kernel If you use a source distribution of Frama C it is possible to disable resp force the in stallation of a plug in of name lt plug in name gt by passing the configure script the option disable lt plug in name gt resp enable lt plug in name Disabling a plug in means it is neither compiled nor installed Forcing the compilation and installation of a plug in against configure s autodetection based default may cause the entire
14. of installation and commands Chapter 4 explains how to work with plug ins Chapter 5 presents the options of the source code pre processor Chapter 6 gives some general options for parametrising analyzers Chapter 7 introduces general services offered by the platform Chapter 8 gives a detailed description of the graphical user interface of Frama C Chapter 9 explains how to report errors via the Frama C s Bug Tracking System Chapter 2 Overview 2 1 What 1s Frama C Frama C is a platform dedicated to the static analysis of source code written in C The Frama C platform gathers several static analysis techniques into a single collaborative extensible framework The collaborative approach of Frama C allows static analyzers to build upon the results already computed by other analyzers in the framework Thanks to this approach Frama C provides very sophisticated tools such as a slicer and dependency analysis 2 2 Frama C as a Static Analysis Tool Static analysis of source code is the science of computing synthetic information about the source code without executing it To most programmers static analysis means measuring the source code with respect to various metrics examples are the number of comments per line of code and the depth of nested control structures This kind of syntactic analysis can be implemented in Frama C but it is not the focus of the project Others may be familiar with heuristic bug fin
15. of the program and related initial conditions main lt function_name gt specifies that all analyzers should treat the function function_name as the entry point of the program lib entry indicates that analyzers should not assume globals to have their initial values at the beginning of the analysis This option together with the specification of an entry point f can be used to analyze the function f outside of a calling context even if it is not the actual entry point of the analyzed code 6 2 Customizing Analyzers The descriptions of the analysis options follow For the first two the description comes from the Value Analysis manual 3 Furthermore these options are very likely to be modified in future versions of Frama C absolute valid range m M specifies that the only valid absolute addresses for reading or writing are those comprised between m and M inclusive This option currently allows to specify only a single interval although it could be improved to allow several intervals in a future version no overflow instructs the analyzer to assume that integers are not bounded and that the analyzed program s arithmetic is exactly that of mathematical integers This option should only be used for codes that do not depend on specific sizes for integer types and do not rely on overflows For instance the following program is analyzed as non terminating in this mode void main void int x 1 while x return
16. 9 2 Exit Status When exiting Frama C has one of the following status O Frama C exits normally without any error 1 Frama C exits because an user input was invalid 2 Frama C exits because the user kills it 3 Frama C exits because the user tries to use an unimplemented feature he should report a feature request on the BTS 4 Frama C exits on an internal error the user should report a bug report on the BTS 5 Frama C exits abnormally on an unknown error the user should report a bug report on the BTS 41 Appendix Changes This chapter summarizes the changes in this documentation between each Frama C release Beryllium 20090902 e First public release 43 BIBLIOGRAPHY Bibliography 1 Patrick Baudin Pascal Cuoq Jean Christophe Filli tre Claude March Benjamin Monate Yannick Moy and Virgile Prevosto ACSL ANSI ISO C Specification Language Version 1 4 Frama C Beryllium implementation October 2009 2 Patrick Baudin Jean Christophe Filli tre Claude March Benjamin Monate Yannick Moy and Virgile Prevosto ACSL ANSI ISO C Specification Language preliminary de sign V1 4 preliminary edition October 2008 Lo 13 Pascal Cuoq and Virgile Prevosto Frama C s value analysis plug in October 2009 http frama c cea fr download value analysis Beryllium 20090902 pdf 4 o Julien Signoles Loic Correnson and Virgile Prevos
17. ading on all architectures and is able to provide better debugging information Use the native compiled version unless you have a reason to use the bytecode one batch vs interactive The interactive version allows to use a GUI to select the set of files to analyze position options launch analyses browse the code and observe analysis results at one s convenience see Chapter 8 for details With the batch version all settings and actions must be provided on the command line This is not possible for all plug ins nor is it always easy for beginners Modulo the limited user interactions the batch version allows the same analyses as the interactive version A batch analysis session consists in launching Frama C in a terminal Results are printed on the standard output The task of analysing some C code being iterative and error prone Frama C provides functionalities to set up an analysis project observe preliminary results and progress until a complete and satisfactory analysis of the desired code is obtained 3 3 Frama C Command Line and General Options The batch and interactive versions of Frama C obey a number of command line options Any option that exists in these two modes has the same meaning in both For instance the batch version can be made to launch the value analysis on the foo c file with the command frama c val foo c Although the GUI allows to select files and to launch the value analysis http ocamlgraph
18. are loaded 3 the saved current project is restored 4 Frama C is replayed with the parameters of the saved current project except for those parameters explicitely set in the current session Consider for instance the following command frama c load foo sav val It loads all projects saved in the file foo sav Then it runs the value analysis in the new current project if and only if it was not already computed at save time Beware that all the existing projects are deleted even if an error occurs when reading the file Thus in the GUI do not hesitate to save the existing projects in some file before loading another file 7 2 Dependencies between Analyses Usually analyses do have parameters see Chapter 6 Whenever values of parameters changes results of the analyses may change In order to not display inconsistent results according to the current value of parameters Frama C automatically discards results of an analysis when one of the analysis parameters changes Consider the two following commands frama c save foo sav ulevel 5 unsafe arrays val foo c frama c load foo sav Frama C runs the value analysis plug in on the file foo c where loops are unrolled 5 times For computing its result the value analysis assumes that accesses in the array are always within the correct bound option unsafe arrays see Section 6 2 Just after Frama C saves the results on file foo sav and exists At loading time
19. d a file name then press Save This file can be reloaded later by using the function Open of the File menu 6 Quit Frama C by using the Quit button in the main window This action generated a journal called frama_c_journal ml If your system supports native dynamic linking it is replayable by running frama c gui load script frama_c_journal ml 8 4 Error Windows An inadequate user input or manipulation or possible internal errors may lead Frama C to report an Error Window The user is informed through an urgent message in foreground complemented with detailed information such as the location of the error in the source code Detailed information is always written in the Frama C console either behind the error window 36 8 4 ERROR WINDOWS Launching analysis Figure 8 6 Setting Analysis Parameters or within the Messages View For instance when the source code provided to Frama C is invalid the message of figure 8 8 comes up 37 CHAPTER 8 THE GRAPHICAL USER INTERFACE RR ala File TIRIN A NO ER al Hpragma Jess1eFloatModel strict requires Oxlp 1000 R1 A R1 0x1p1000 a Ox1p 1000 R2 a R2 0x1p1000 behavior default ensures result gt 0 requires Oxlp 1000 lt Rl lt Ox1p1000 amp amp gt 4 Ox1p 1000 lt R2 lt Ox1p1000 double R_ges double R1 double R2 ensures result gt O 1 far 3 double R_ges double R1 double R2 d t 2 E Y pt nad dep
20. ding tools These tools take more of an in depth look at the source code and try to pinpoint dangerous constructions and likely bugs locations in the code where an error might happen at run time These heuristic tools do not find all such bugs and sometimes they alert the user for constructions which are in fact not bugs Frama C is closer to these heuristic tools than it is to software metrics tools but it has two important differences with them it aims at being correct that is never to remain silent for a location in the source code where an error can happen at run time And it allows its user to manipulate functional specifications and to prove that the source code satisfies these specifications Frama C is not the only correct static analyzer out there but analyzers of the correct family are less widely known and used Software metrics tools do not guarantee anything about the behavior of the program only about the way it is written Heuristic bug finding tools can be very useful but because they do not find all bugs they can not be used to prove the absence of bugs in a program Frama C on the other hand can guarantee that there are no bugs in a program no bugs meaning either no possibility of a run time error or even no deviation from the functional specification the program is supposed to adhere to This of course requires more work from the user than heuristic bug finding tools usually do but some 11 CHAPTER 2 OVERVIEW
21. e dynamic linking feature of OCaml It is only available in the most recent versions of OCaml at least 3 11 0 and only on a subset of supported platforms Gtk related packages GTK version 2 4 or higher GtkSourceView version 1 x as well as LabIGTK version 2 12 or higher are required for building the graphical user interface GUI of Frama C http www gnu org software make http caml inria fr http www gtk org http projects gnome org gtksourceview http wwwfun kurims kyoto u ac jp soft 1s1 lablgtk html 15 CHAPTER 3 GETTING STARTED OcamlGraph package Frama C will make use of OcamlGraph if already installed in version 1 3 or higher Otherwise Frama C will install a local and compatible version of this package by itself This dependency is thus non mandatory for Frama C 3 2 One Framework Four Executables Frama C installs four executables namely e frama c native compiled batch version e frama c byte bytecode batch version e frama c gui native compiled interactive version e frama c gui byte bytecode interactive version The differences between these versions are described below native compiled vs bytecode native executables contain machine code while bytecode executables contain machine independent instructions which are run by a bytecode in terpreter The native compiled version is usually ten times faster than the bytecode one The bytecode version supports dynamic lo
22. frama Software Analyzers User Manual 2 4 4 1 0 a ne 1 o 0 kes 2 jul np MEN duc fi Sa co List Frama C User Manual Beryllium release Loic Correnson Pascal Cuog Armand Puccetti and Julien Signoles CEA LIST Software Reliability Laboratory Saclay F 91191 2009 CEA LIST CONTENTS Contents Foreword 7 1 Introduction 9 1 1 Organization of the Document 26 6 1 4 e shee ew eRe eee eR eS 2 Overview 11 21 Whatis FAM ek tk wk ee Eu nun HER ERA eR AH EES EHS 11 2 2 Frama C as a Static Analysis Tool 0 nn 11 2 2 1 Frama C as a Lightweight Semantic Extractor Tool 12 2 2 2 Frama C for Formal Verification of Critical Software 12 2 3 Frama C as a tool for C programs 0 0 0 0000022 2G 12 2 4 Frama C as an Extensible Platform n a oaoa a a 12 2 5 Frama C as a Collaborative Platform 13 2 6 Frama C as a Development Platform a a a a 13 3 Getting Started 15 od MEM A se segr eh aeaa AA 15 3 2 One Framework Four Executables a 16 3 3 Frama C Command Line and General Options 16 dad Getme Help os sm cesa as a A A 17 3 3 2 Frama C Version a baw wee eR nn ea a a A 17 3 3 3 Verbosity and Debugging Levels 17 3 3 4 Getting time hk wR BRA wae PELE 18 3 3 5 Inputs and Outputs of source code 2 2 2 m m nn nn nn 18 3 4 The share directory cma
23. have information about them 8 3 Example Let us go through a simple example to illustrate how to handle projects from the GUI Starting from an empty Frama C view as show above in Figure 8 1 we do the following steps 1 Create a new project with one valid C file named f2 c click on button New to open the source file management view Then add new files to the project by navigating to the right directory and selecting the desired files on the left side and press buttons Add the source file and New to create a project See figure 8 4 Select source files Recently Used a 07 01 09 puccetti E Thursday 3 Desktop 354 Thursday E File System UDISK BIER 09 19 08 E users max c Thursday max2 c 02 19 09 more uninit c 09 16 08 Source files Figure 8 4 The Source File Management View 2 The source is normalized and the source code can be displayed Clicking on the file name f2 c of the file tree leads to a view similar to Figure 8 5 3 Perform a values analysis on function main press on the button Execute of the main view to open the analysis window This window allows the user to finely tune the parameters of every analysis They are therefore grouped by analysis function and 35 CHAPTER 8 THE GRAPHICAL USER INTERFACE w a de L 8 x File View Analyses Change project Help a gt HH Find New Execute Quit Loy Source file loccurrence Slic
24. ing pragma JessieFloatModel strict requires Ox1p 1000 R1 a R1 Ox1p1000 a Ox1p 1000 R2 A R2 Ox1p1000 behavior default ensures result gt 0 double R_ges double R1 double R2 double _retres _retres 1 0 1 0 R1 1 0 R2 return __retres int main void int __retres j 0 R R ges double 100 double 200 __retres 0 return __retres gt Slicing Impact Mi Enable 7 I Rara nn Information Messages Console C Follow focus Functions R ges main WP very experimental E use bottom Model Behavior gt Metrics Measure sloc calls Figure 8 5 Displaying the Normalized Source displayed with the same name as in batch mode For performing a values analysis we need to select at least the option val in the category value analysis as in figure 8 6 Leaving other options to their default value we may launch the values analysis Clicking button Execute of the dialog box closes it and starts the desired analysis 4 Let us examine the results of the analysis by using the source views Click on file 2 c on the file tree view and click on variable R of the center source view leading to display the computed value at the bottom as in the figure 8 7 5 Save work in a file by clicking on the item Save of the menu File In the opened dialog box select a directory an
25. l session Journals are usually used for the three different purposes described thereafter e Replay easily a given set of analysis operations in order to reach a certain state Once the final state is reached further analyses can be performed normally Beware that journals may be source dependent and thus can not necessarily be reused on different source codes to perform the same analyses e Act as a macro language for plug in developers They can perform some wished actions on the GUI to generate a journal and then adapt it to perform a more general but similar task e Debugging In the GUI a journal is always generated even when an error occurs The output journal usually contains information about this error T hus it provides an easy way to reproduce the very same error Consequently it is advised to attach the journal when reporting an error in the Frama C BTS see Chapter 9 Journalisation is always enabled in graphical mode and disabled in batch mode This behaviour may be customized by using the option journal enable resp journal disable that generates resp does not generate a journal upon exit of the session 29 Chapter 8 The Graphical User Interface 8 1 The Frama C Main Window Upon launching Frama C in graphical mode the following main window is displayed fig ure 8 1 File View Analyses Change project Menu Bar Shortcut Buttons New Execute Quit Source file Occurrence Slici
26. ment Guide 4 14 Chapter 3 Getting Started This chapter describes how to install Frama C and what this installation provides 3 1 Installation The Frama C platform is distributed as source code Binaries are also available for popular architectures All distributions include the Frama C kernel and a base set of open source plug ins It is usually easier to install Frama C from one of the binary distributions than from the source distribution The pre compiled binaries include many of the required libraries and other dependencies whereas installing from source requires these dependencies already to have been installed The dependencies of the Frama C kernel are as follows Each plug in may define its own set of additional dependencies Instructions for installing Frama C from source may be found in the file INSTALL of the source distribution A C pre processor is required for using Frama C By default Frama C tries to use gcc C E I as pre processing command but this command can be customized see Sec tion 5 1 A Unix like compilation environment is mandatory and shall have at least the tool GNU make version 3 81 or higher as well as various POSIX commands The OCaml compiler is required both for compiling Frama C from source and for compiling additional plug ins Version 3 10 2 or higher must be used Support of some plug ins in native compilation mode see Section 3 2 requires the so called nativ
27. n follow the progress of the analysis by scrolling this view which automatically disappears once the analysis is complete to leave room for the Main Window The Splash Information View shows the same analysis traces as if Frama C was run in batch mode When closed its contain is copied into the Console pages on the messages view 8 2 Main Functions 8 2 1 The Menu Bar The menu bar is organised into logically structured menus The File Menu proposes functions for managing the current session Function New creates a new project in the current session Function Open opens an existing state file stored on disk This clears all projects already open in the current session See Section 7 1 3 32 8 2 MAIN FUNCTIONS Splash o ESET kernel preprocessing with gece E C DNDEBUG D 86 64 D GNU DBASILE XEN PPC hormne puccetti serveur xen 3 0 3 top include asm uaccess h 28 kernel warning Return stateme horne puccetti serveur xen 3 0 3 xen includefasm hvm hvm h 187 kernel warning Return state kernel preprocessing with gee E C DNDEBUG D 86 64 D GNU DBASILE XEN PPC kernel preprocessing with gcc E C DNDEBUG D x86 64 D GNU DBASILE XEN PPC horne puccetti serveur xen 3 0 3 top include asm uaccess h 28 kernel warning Return stateme horne puccetti serveur xen 3 0 3 xen includefasm hvm hvm h 187 kernel warning Return state cea_common h 249 kernel warning Body of function CEAmake_monito
28. ng Please select a file in the left panel or start a new project File Tree Normalized Source Code View Original Source Code View v Slicing E PESE Y Impact Plug ins View Y Enable ee gt Information Messages Console O Slicing after impact te O Follow focus Y Metrics Measure sloc calls if loops L Messages View goto assigns Ptr Fct Proto Y Occurrence IS Figure 8 1 Initial View From top to bottom the window is made of several separate sub parts namely The Menu Bar organizes the highest level functions of the tool into structured categories Plug ins may also add their own entries here for instance the plug in Syntactic Call graph add the entry called View 31 CHAPTER 8 THE GRAPHICAL USER INTERFACE Shortcut Buttons give access to the main functions of the tool These are usually present in one menu of the menu bar Plug ins may also add their own entries here The File Tree provides a tree like structure of the source files involved in the current anal ysis Sources are structured as c and h source files that are in turn structured into functions Clicking on a file name or function name displays the corresponding source code Furthermore plug ins may display specific information for each file and or func tion The normalized and original source code views display the source code of the current
29. nsions The former option loads the specified OCaml object files into the Frama C runtime while the latter tries to compile the source files before linking them to the Frama C runtime The load script option requires the OCaml compiler that was used to compile Frama C to be available In general dynamic plug ins must be compiled with the very same OCaml compiler than Frama C was and against a consistent Frama C installation Loading will fail and a warning will be emitted at launch if this is not the case With the extension exe on Windows OS 20 Chapter 5 Preparing the Sources This chapter explains how to specify the source files that form the basis of an analysis project and describes options that influence parsing 5 1 Pre processing the Source Files The list of files to analyse must be provided on the command line An alternative is to choose the files interactively in the GUI Files with the i suffix are assumed to be already pre processed C files Frama C pre processes the other files with the following command gcc C E I The option cpp command may be used to change the default pre processing command If patterns 1 and 42 do not appear in the provided command the pre processor is invoked in the following way lt cmd gt o lt output file gt lt input file gt In this command lt output file gt is chosen by Frama C while lt input file gt is one of the filenames provided by the user It is
30. o a file If the use never chooses such a file a dialog box is opened for choosing one Function Save as saves all current projects into a file chosen from a dialog box Function Quit exits the current Frama C session A journal is generated at this time except if the option disable journal was provided on the command line see Section 7 3 The Analyses Menu provides the main functions for running new analyses The button Execute opens the Analysis Configuration Window shown Figure 8 3 that groups all options of the kernel and plug ins within a single interface Laun xt x Customize parameters then click on Execute kernel b Finder gt Postdominators and postdominators gt from analysis gt impact b inout b jessie gt Itl to acsl gt metrics b occurrence gt pdg b scope gt security gt semantic callgraph t semantic constant folding gt slicing gt sparecode b syntactic callgraph b users value analysis b wp E cancel 353 Execute Figure 8 3 The Analysis Configuration Window Once the parameters set the user is invited to click on the Execute button to confirm the parameters and execute the activated analyses if necessary Notice that upon opening the Configuration Window some parameters are highlighted in red indicating which parameters have been modified previously with respect to their default values The Change Project Menu allows to switch between pr
31. ojects in the same session Indeed several projects may coexist during a Frama C session possibly generated from a single initial project by performing a series of analyses A typical example is when slicing the source code that generates a new project once done successfully Changing project updates all views in the main window The Help Menu is located on the right extreme of the menu bar Currently it contains one function to display the current version The precise version its authors its compilation date the applicable software license and the credits are shown 34 8 3 EXAMPLE 8 2 2 The Shortcut Buttons The upper button row groups major functions among those found in the menus that we described before Buttons New Execute and Quit act as shortcuts to the functions with the same name Button Stop allows to halt the running analyses and restore Frama C in the last enable valid configuration 8 2 3 The Contextual Menu As said before the normalized source view is the preferred view for interacting with the analysis tools as this one contains the code representation that is manipulated internally by the analysis tools In this view the user can select an object for instance a C statement or a C expression and call up the Contextual Menu right mouse click The list of available actions depends on the kind of the selected object These actions are plug in specific So the reader may refer to each plug in documentation to
32. r_table falls through Adi kernel preprocessing with gcc E C DNDEBUG D 86 64 D GNU DBASILE XEN PPC kernel preprocessing with gee E C DNDEBUG D 86 64 D GNU DBASILE XEN PPC horne puccetti serveur xen 3 0 3 top include asm uaccess h 28 kernel warning Return staterne horne puccetti serveur xen 3 0 3 xen include asm hvm hvm h 187 kernel warning Return state kernel preprocessing with gcc E C DNDEBUG D 86 64 D GNU DBASILE XEN PPC hormne puccetti serveur xen 3 0 3 top include asm uaccess h 28 kernel warning Return stateme horne puccetti serveur xen 3 0 3 xen includefasm hvm hvm h 187 kernel warning Return state horne puccetti serveur xen 3 0 3 top include asmyio h 22 kernel warning dropping duplicate de horne puccetti serveur xen 3 0 3 top include asmyio h 22 kernel warning dropping duplicate de hormme puccetti serveur xen 3 0 3 top include asmyio h 22 kernel warning dropping duplicate de value Computing for function cea mainl INITIAL STATE value Computing globals values cea x86 setup c 173 value could not find a size for array horne puccetti serveur xen 3 0 3 xen includefasm desc h 158 value could not find a size for arr es i RPS E Phi lm mem eee arm m y rms Memo veda formos Emos an ra In Te ml rm l Al el m m Em mim Lar mh E E E Figure 8 2 Splash Information View 33 CHAPTER 8 THE GRAPHICAL USER INTERFACE Function Save saves all the current projects int
33. reak continue and switch statements This op tion is automatically set by some plug ins that cannot handle these kinds of statements This option is set by default ulevel lt n gt unrolls all loops n times This is a purely syntactic operation Loops can be unrolled individually by inserting the UNROLL pragma just before the loop state ment Do not confuse this option with plug in specific options that may also be called unrolling 3 Below is a typical example of use Q loop pragma UNROLL LOOP 10 for i 0 i lt 9 itt 5 4 Testing the Source Code Preparation If the steps up to normalization succeed the project is then ready for analysis by any Frama C plug in It is possible to test that the source code preparation itself succeeds by running Frama C without any option 22 5 4 TESTING THE SOURCE CODE PREPARATION frama c lt input files gt If you need to use some options for pre processing or normalizing the source code you can use the option type check for the same purpose For instance frama c cpp command gcc C E I x c type check filel src file2 i 23 Chapter 6 Analysis Options The analysis options described in this chapter provide hypotheses that influence directly the behavior of analyzers For this reason the user must understand them and the interpretation the plug ins he uses have of them 6 1 Entry Point The following options define the entry point
34. s For instance verbose O slicing verbose 1 runs Frama C quietly except for the slicing plug in 17 CHAPTER 3 GETTING STARTED 3 3 4 Getting time The option time lt file gt appends user time and date to the given log lt file gt at exit 3 3 5 Inputs and Outputs of source code The following options deal with inputs and outputs of analyzed source code print causes Frama C s representation for the analyzed source files to be printed as a single C program see Section 5 3 ocode lt file name gt redirects all output code to the designated file keep comments keeps C comments in lined in the code obfuscate can only be used alone to obfuscate C code Once done Frama C exits 3 4 The share directory Frama C looks for all its files installed manuals configuration files C modelization libraries etc in a single directory The location of this directory is chosen at configure time configure option datarootdir Frama C can look for files in a different location than the preconfig ured one by setting the environment variable FRAMAC_SHARE to the path of the directory to use The option print share path causes Frama C to print the path of the current share direc tory 18 Chapter 4 Working with Plug ins The Frama C platform has been designed to support third party plug ins In the present chapter we present how to configure compile install run and update such extensions This chapter does
35. selected element of the file tree and its normalised code see Section 5 3 The user may select objects in the normalized source code view to obtain detailed information on it and activate further functions through the Menu Bar the Shortcut Buttons or the Contextual Menu described below When selecting an object Frama C shows its counterpart in the original source code Note that only the normalized source view is interactive The Plug ins View allows the user to interact with the plug ins by using a specific interface For instance such a view is used in order to modify some graphical effects such as highlighting or strike throughs using radio buttons The interface of each plug in can be hidden The Messages View contains three different pages namely the information page which provides brief details on the currently selected object the Messages page shows alarms that the last analysis has produced Alarms are structured and may have different degrees of urgency Please refer to the specific documentation of each analyzer for details the Console page displays messages to users That is the very same output than the one shown in batch mode Displaying the GUI when running Frama C may take a significant time In such a case Frama C does not display immediately the above mentioned main window but first informs the user about progress by means of a temporary Splash Information View see figure 8 2 The user ca
36. ses has its own specific documentation 3 Additional plug ins can be provided by third party developers and installed separately from the kernel 2 5 Frama C as a Collaborative Platform Frama C s analyzers collaborate with each other Each plug in may interact with other plug ins of his choosing The kernel centralizes information and conducts the analysis This makes for robustness in the development of Frama C while allowing a wide functionality spectrum For instance the Slicing plug in uses the results of the Value Analysis plug in and of the Functional Dependencies plug in Analyzers may also exchange information through ACSL annotations 2 A plug in that needs to make an assumption about the behavior of the program may express this assumption as an ACSL property Because ACSL is the lingua franca of all plug ins another plug in can later be used to establish the property With Frama C it will be possible to take advantage of the complementarity of existing analysis approaches It will be possible to apply the most sophisticated techniques only on those parts of the analyzed program that require them The low level constructs can for instance eftectively be hidden from them by high level specifications verified by other adapted plug ins Note that the sound collaboration of plug ins on different parts of a same program that require different modelizations of C is work in progress At this time a safe restriction for
37. ssary for normal use but it may be generated with the command make static External dynamic plug ins may be configured and compiled with the Frama C kernel by using the option enable external lt path to plugin gt This option may be passed several times 4 4 Using Plug ins All Frama C plug ins define the following set of common options lt plug in name gt help prints out the list of options of the given plug in lt plug in name gt verbose lt n gt sets the level of verbosity to some positive integer n A value of 0 means no information messages Default is 1 lt plug in name gt debug lt n gt sets the debug level to a positive integer n The higher this number the more debug messages are printed Debug messages do not have to be understandable by the end user This option s default is O no debugging message Please refer to each plug in s documentation for specific options At launch Frama C loads all dynamic plug ins it finds It searches for them in directories indicated by frama c print plugin path This directory list is pre configured at compila tion and may be changed by setting the environment variable FRAMAC_PLUGIN Frama C can locate plug ins in additional directories by using the option add path lt paths gt Yet another solution to load a dynamic plug in is to set the load module lt files gt or load script lt files gt options using in both cases a comma separated list of file names without exte
38. this purpose Category select as appropriate Reproducibility select as appropriate Severity select the level of severity Levels are shown in increasing order of severity Profile or Platform OS and OS Version enter your hardware and OS characteristics Product Version and Product Build this can be obtained through the command frama c version see Section 3 3 2 Summary give a brief one line description of the nature of your bug Description first explain the actual behavior that is what you actually observe on your system Then describe your expected behavior of Frama C that is the results you expect instead A bug is sometimes due to a misunderstanding of the tool s behaviour or a misunderstanding of its results so providing both behaviors is an essential part of the report Please do clearly separate both parts in the description You can also have a look at the associated Frama C wiki http bts frama c com dokuwiki doku php id mantis frama c start 39 CHAPTER 9 REPORTING ERRORS Report Issue Frama C Bug Tracking System SeaMonkey File Edit View Go Bookmarks Tools Window Help Q 7 PA http bts frama c com bug_report_page php a NINA Logged in as puccetti puccetti reporter 2009 09 15 16 18 CEST Details Advanced Report E public private check to report more issues Mantis 1 1 6 7 Copyright 2000 2008 Mantis Group benjamin monategicea fr Figure 9
39. to Frama C Plug in Development Guide September 2009 http frama c cea fr download plugin developer Beryllium 20090902 pdf 45 absolute valid range 25 add path 20 annot 22 Batch version 16 Bytecode 16 C pre processor 15 constfold 22 continue annot error 22 cpp command 21 cpp extra args 21 datarootdir 18 debug 17 disable journal 34 frama c 16 frama c gui 16 frama c gui byte 16 frama c byte 16 FRAMAC_LIB 20 FRAMAC_PLUGIN 20 FRAMAC_SHARE 18 GTK 15 GtkSourceView 15 help 17 Installation 15 Interactive version 16 journal disable 29 journal enable 29 journal name 29 keep comments 18 keep switch 22 kernel debug 17 kernel help 17 kernel verbose 17 Lablgtk 15 INDEX 47 Index lib entry 25 load 28 load module 20 load script 20 29 machdep 22 main 25 Native compiled 16 obfuscate 18 OCaml compiler 15 OcamlGraph 16 ocode 18 Options 16 overflow 25 Plug in Dynamic 19 External 19 Internal 19 Static 19 pp annot 21 Pragma UNROLL 22 print 18 22 print lib path 20 print plugin path 20 print share path 18 20 quiet 17 safe arrays 26 save 28 simplify cfg 22 time 18 type check 23 ulevel 22 unsafe arrays 26 unspecified access 26 verbose 17 INDEX version 17 with all static 19 48
40. ts can also be considered as formal specifications For instance the list of global variables that a function is supposed to read or write to is a formal specification Frama C can compute this information automatically from the source code of the function allowing you to verify that the code satisfies this part of the design document faster and with less risks than a code review 2 3 Frama C as a tool for C programs Frama C analyses C programs The C source code is assumed to follow the C99 ISO standard C comments may contain ACSL annotations 2 used as specifications to be interpreted by Frama C The subset of ACSL currently interpreted in Frama C is described in 1 Furthermore each analyzer may define the subsets of C and ACSL that it understands as well as introduce specific limitations and hypotheses Please refer to each plug in s documentation 2 4 Frama C as an Extensible Platform Frama C is extensible 12 2 5 FRAMA C AS A COLLABORATIVE PLATFORM It is is organized with a plug in architecture comparable to that of the Gimp or Eclipse each analyzer comes in the form of a plug in and is connected to the platform itself or kernel Several ready to use analyses are included in the Frama C distribution This manual covers the set of features common to all plug ins It does not cover use of the plug ins that come in the Frama C distribution Value Analysis Functional Dependencies etc Each of these analy
41. using plug in collaboration is to limit the analyzed program and annotations to those C and ACSL constructs that are understood by all involved plug ins 2 6 Frama C as a Development Platform Frama C may be used for developing new analyses The collaborative and extensible approach of Frama C allows powerful plug ins to be written with relatively little effort There are a number of reasons for a user of Frama C also to be interested in writing his her own plug in e a custom plug in can emit very specific queries for the existing plug ins and in this way obtain information which is not easily available through the normal user interface e a custom plug in has more latitude for finely tuning the behavior of the existing analyses e some analyses may offer specific opportunities for extension If you are a researcher in the field of static analysis using Frama C as a testbed for your ideas is a choice to consider You may benefit from the ready made parser for C programs with ACSL annotations The results of existing analyses may simplify the problems that are orthogonal to those you want to consider in particular the Value Analysis provides sets of 13 CHAPTER 2 OVERVIEW possible targets of every pointer in the analyzed C program And lastly being available as a Frama C plug in increases your work s visibility among existing industrial users of Frama C The development of new plug ins is described in the Plug in Develop
42. when the evaluation of an expression depends on the order in which its sub expressions are evaluated For instance This occurs with the following piece of code MD 1 amp i i p 1 1 e i i p j In this code it is unclear in which order the elements of the right hand side of the last assignment are evaluated Indeed the variable j can get any value as i and p are aliased The unspecified access option aims at warn against such ambiguous situations 26 Chapter 7 General Kernel Services This chapter presents some important services offered by the Frama C platform 7 1 Projects A Frama C project groups together one source code with the states parameters results etc of the Frama C kernel and analyzers In one Frama C session several projects may exist at the same time while there is always one and only one so called current project in which analyses are performed Thus projects help to structure a code analysis session into well defined entities For instance it is possible to perform one analysis on the same code with different parameters and to compare the obtained results It is also possible to extract a program p from an initial program p and to compare the results of an analysis run separately on p and p 7 1 1 Creating Projects A new project is created in the following cases e at initialization time a default project is created or e the menu item or button New of the graphical
43. zation phase These transformations aim at making further work easier for the analyzers Analyses take place exclusively on the normalized version of the source code The normalized version may be printed by using the option print see Section 3 3 5 The following options allow to customize the normalization annot forces Frama C to interpret ACSL annotations This option is set by default and is only found in its opposite form no annot which prevents interpretation of ACSL annotations constfold performs a syntactic folding of constant expressions For instance the expression 1 2 is replaced by 3 keep switch preserves Switch statements in the source code Without this option they are transformed into if statements An experimental plug in may forgot the treatment of the switch construct and require this option not to be used Other plug ins may prefer this option to be used because it better preserves the structure of the original program machdep lt machine architecture name gt defines the target platform The default value is a x86 32bits platform Analyzers may take into account the endianness of the target the size and alignment of elementary data types and other architecture compilation parameters The machdep option provides a way to define all these parameters consis tently in a single step The list of supported platforms can be obtained by typing frama c machdep help simplify cfg allows Frama C to remove b
Download Pdf Manuals
Related Search