Home

User Manual - Frama-C

1. struct s 4 int a int b 2 int c F void main struct s v 4 v b 1 1 v b 2 4 The opposite option called safe arrays is set by default With safe arrays the two accesses to v are considered invalid Accessing v b 2 or v b 3 remains incorrect regardless of the value of the option unspecified access may be used to check 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 int i j p i p amp i j i p Be sure to enclose it in single quotes or your shell might expand it leading to unexpected results 34 6 3 CUSTOMIZING ANALYZERS 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 warns against such ambiguous situations More precisely unspecified access detects potential concurrent write accesses or a write access and a read access over the same location that are not separated by a sequence point Note however that this option does not warn against such accesses if they occur in an inner function call such as in the following example int x int O return x int gO return fO x Here the x might be incremented by g before or after the call to f but since the two write accesses occur
2. It can be modified by using the option journal name 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 as the ones computed in the original session Journals are usually used for the three different purposes described thereafter e Easily replay 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 may 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 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 Thus 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 10 By default a journal is generated upon exit of the session only whenever Frama C crashes in graphical mode In all other cases no journal is generated This behavior may be customized by using the option journal enable resp journal disable that generates resp does not generate a journal upon exiting the session
3. for instance because it does not consider functions that can modify globals While convenient in a wide range of cases this can be averted by writing a custom function contract for the contentious prototypes A function prototype is a function declaration that provides argument types and return type but lacks a body Results here include the return value and the formal modifiable parameters The rest of this chapter will examine the treatment plug ins can make of code annotations and in particular what kind of information can be attached to them 37 CHAPTER 7 PROPERTY STATUSES 7 2 Properties and the Statuses Thereof A property is a logical statement bound to a precise code location A property might originate from e an ACSL code annotation e g assert p i p i lt INT MAX Recall from the previous section that annotations can either be written by the user or generated by the Frama C plug ins or kernel e a plugin dependent meta information such as the memory model assumptions Consider a program point and call T the set of traces that run through More precisely we only consider the traces that are coming from the program entry point see option main in chapter 6 A logical property P is valid at if it is valid on all t T Conversely any trace u that does not validate P stops at 2 properties are blocking As an example a property might consist in a statement pli x pli l
4. I FRAMAC_SHARE libc to the preprocessor com mand and also nostdinc if cpp gnu like is set 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 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 normalization phase These transformations aim at making further work easier for the analyzers Analyses usually take place on the normalized version of the source code The normalized version may be printed by using the option print see Section 3 3 7 Normalization gives a program which is semantically equivalent to the original one except for one point Namely when the specification of a function f that is only declared and has no ACSL assigns clause is required by some analysis Frama C generates some assigns clause based on the prototype of the form of this clause is left unspecified Indeed as mentioned in the ACSL manual 2 assuming that f can write to any location in the memory would amount to stop any sem
5. i lt 50 i tli fi 21 i 22 loop invariant A lt int j j A A A O e loop invariant As j A j lt 100 a pa assigns j tiA o loop assigns j t A 99 i ski while j lt 100 t j g j j a for int j A j lt 100 j t j g j vWP 27 assert forall integer k lt k lt 50 gt P t k Model Store O assert VZk 0 lt ka k lt 50 P t k EN q return Prover Alt Ergo J Er 2 _ _ 31 int T 100 RTE U Split C invariants C Trace i 32 int T 100 a i Scripts Timeout 10 Process 4 gt void main void 33 void main void 34 job T 50 Y Slicing Plug in view job T 50 35 job T 48 Activate _ return E Information Messages Console Properties WP Proof Obligations File home ftk Projects fc elements demo wp c Y Impact Functions job main aoa Declared variables f g Message view Marte Variables T Enable Slicing after impact C Follow focus Y Metrics Measure Figure 9 1 Initial View From top to bottom the window is made of several separate sub parts The menu bar organizes the highest level functions of the tool into structured categories Plug ins may also add their own entries in the Analyses menu 45 CHAPTER 9 GRAPHICAL USER INTERFACE The toolbar gives access to the main functions of the tool They are usually present in one menu of the menu bar Plug ins may also add their own ent
6. while setting it 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 0 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 shortname gt verbose resp lt plug in shortname gt debug set the level of verbosity resp debugging of the kernel and particular plug ins When both the global level of verbosity resp debug ging and a specific one are modified the specific one applies For instance verbose O slicing verbose 1 runs Frama C quietly except for the slicing plug in It is also possible to choose which categories of message should be displayed for a given plugin See section 6 2 for more information 3 3 6 Getting time The option time lt file gt appends user time and date to the given log lt file gt at exit 3 3 7 Inputs and Outputs of Source Code The following options deal with the output of analyzed source code print causes Frama C s representation for the analyzed source files to be printed as a single
7. To enable all 33 CHAPTER 6 PLATFORM WIDE ANALYSIS OPTIONS categories use the wildcard x Categories can have subcategories defined by a colon in their names For instance a b c is a subcategory c of a b itself a subcategory of a Enabling a category will also enable all its subcategories The two following options modify the behavior of the output messages add symbolic path takes a list of the form name path name path in argument and replace each path by name when displaying file locations in messages permissive performs less verification on validity of command line options 6 3 Customizing Analyzers The descriptions of the analysis options follow For the first two the description comes from the Value Analysis manual 7 Note that 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 unsafe arrays can be used when the source code manipulates n dimensional arrays or arrays within structures in a non standard way With this option accessing indexes that are out of bounds will instead access the remainder of the struct For example the code below will overwrite the fields a and c of v
8. also available on the web or upon simple inquiry to the Frama C team 16 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 on C files By default Frama C tries to use gcc C E I as pre processing command but this command can be customized see Section 5 1 If you do not have any C pre processor you can only run Frama C on already pre processed i file A C compiler is required to compile Frama C kernel 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 libraries and header files The OCaml compiler
9. bytecode executables contain machine independent instructions which are run by a bytecode interpreter The native compiled version is usually ten times faster than the bytecode one The bytecode version supports dynamic loading 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 is a GUI that can be used 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 9 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 http www gtk org nttp projects gnome org gtksourceview http library gnome org devel libgnomecanvas Shttp wwwfun kurims kyoto u ac jp soft 1s1 lablgtk html http ocamlgraph 1ri f
10. config and lt plug in shortname gt config as well as new environment variable FRAMAC_CONFIG e Getting Started new options session and lt plug in shortname gt session as well as new environment variable FRAMAC_SESSION e Getting Started document option unicode e General Kernel Services clarify when saving is done 53 APPENDIX A CHANGES Fluorine 20130 01 e Getting Started update installation requirements e Customizing Analyzers document the following new options warn signed overflow warn unsigned overflow warn signed downcast and warn unsigned downcast e Preparing the Sources document new option enums Oxygen 20120901 e Analysis Option better documentation of unspecified access e Preparing the Sources better documentation of pp annot e Preparing the Sources pragma UNROLL LOOP is deprecated in favor of UNROLL e Preparing the Sources document new normalization options warn decimal float warn undeclared callee and keep unused specified functions e General Kernel Services document special cases of saving and journalisation e Getting Started optional Zarith package e Getting Started new option lt plug in shortname gt share Nitrogen 20111001 e Overview report on Frama C usage as an educational tool e Getting Started exit status 127 is now 125 127 and 126 are reserved by POSIX e Getting Started update options for controlling display o
11. how to configure compile install run and update such extensions This chapter does not deal with the development of new plug ins see the Plug in Development Guide 12 Neither does it deal with usage of plug ins which is the purpose of individual plug in documentation see e g 7 4 3 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 gt Disabling a plug in means it is neither compiled nor installed F
12. immediately start displaying the results in the GUI Any option requiring an argument may use the following format option_name value Parameterless Options Most parameterless options have an opposite option often writ ten by prefixing the option name with no For instance the option unicode for using the Unicode character set in messages has an opposite option 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 op posite of option wp print is wp no print When prefixing an option name by no is meaningless the opposite option is usually renamed For instance the opposite option of journal enable is journal disable Use the options kernel help and lt plug in name gt help to get the opposite option name of each parameterless option String Options 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 Set Options Some options e g option cpp extra args accept a set of comma separated values as argument Each value may be prefix by resp to indicate that this value must be added to resp deleted from the set When neither is specified is added by default 19 CHAPTER 3 GETTING STARTED
13. is required both for compiling Frama C from source and for compiling additional plug ins Version 3 12 1 or higher must be used Support for some plug ins in native compilation mode see Section 3 2 requires the so called native dynamic linking feature of OCaml It is not available in all supported platforms Inttp www gnu org software make nttp caml inria fr 17 CHAPTER 3 GETTING STARTED Gtk related packages GTK version 2 4 or higher GtkSourceView version 2 x Gnome Canvas version 2 x as well as LablGtk version 2 14 or higher are required for building the Graphical User Interface GUI of Frama C OcamlGraph package Frama C will make use of OcamlGraph if already installed in version 1 8 2 with x gt 5 Otherwise Frama C will install a local and compatible version of this package by itself This dependency is thus non mandatory for Frama C Zarith package Frama C will make use of Zarith if installed Otherwise Frama C will make use of a functionally equivalent but less efficient library 3 2 One Framework Four Executables Frama C installs four executables namely frama c natively compiled batch version frama c byte bytecode batch version frama c gui natively compiled interactive version 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
14. 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 Functional Verification Slicing etc Each of these analyses has its own specific documentation 7 4 3 Additional plug ins can be provided by third party developers and installed separately from the kernel Frama C is thus not limited to the set of analyses initially installed For instance it may be extended with the E ACSL plug in 11 8 which instruments the program in order to check annotations at runtime In this way Frama C is not restricted to static analysis of source code but also provides dynamic analysis 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 Fr
15. menu proposes items for managing the current session Item Source files changes the analyzed files of the current project Item Reparse reloads the source files of the current project from the disk reparses them and restarts the analyses that have been configured Item Save session saves all the current projects into a file If the user has not yet specified such a file a dialog box is opened for selecting one Item Save session as saves all current projects into a file chosen from a dialog box Item Load Session opens a previously saved session This fully resets the current session see Section 8 1 3 Item Quit exits Frama C without saving The project menu displays the existing projects allowing you to set the current one You can also perform miscellaneous operations over projects creating from scratch dupli cating renaming removing saving etc The analyses menu provides items for configuring and running plug ins e Item Configure and run analyses opens the dialog box shown Figure 9 2 that allows to set all Frama C parameters and to re run analyses according to changes Launching analysis Customize parameters then click on Execute gt kernel gt GUI gt WP gt aorai gt dominators gt from analysis gt impact gt inout gt metrics gt obfuscator gt occurrence gt pdg gt postdominators gt report gt rte annotation gt scope gt security slicing gt semantic callgraph gt
16. status is False and all dependencies have the consolidated status surely valid O _ inconsistent when there exist two conflicting consolidated statuses for the same property for instance with values surely_valid and surely_invalid This case may also arise when an invalid cyclic proof is detected This is symptomatic of an incoherent axiomatization or an incomplete status considered valid when there is no possible way to prove the property e g the post condition of an external function We assume this property will be validated by external means O valid_under_hyp when the local status is True but at least one of the dependencies has consolidated status unknown This is typical of proofs in progress invalid_under_hyp when the local status is False but at least one of the depen dencies has status unknown This is a telltale sign of a dead code property or of an erroneous annotation and finally unknown_but_dead when the status is locally Maybe but in a dead or incoherent branch O valid_but_dead when the status is locally True but in a dead or incoherent branch O invalid_but_dead when the status is locally False but in a dead or incoherent branch 39 CHAPTER 7 PROPERTY STATUSES The dependencies are meant as a guide to safety engineers They are neither correct nor complete and should not be relied on for formal assessment purposes In particular as long as partial proofs exis
17. 1 ulevel 20 28 30 42 43 ulevel force 30 unicode 21 42 44 unsafe arrays 34 unspecified access 34 val 20 val use spec 20 verbose 21 42 44 version 19 49 warn decimal float 30 warn signed downcast 35 warn signed overflow 35 warn undeclared callee 30 warn unsigned downcast 35 62 INDEX warn unsigned overflow 35 with all static 25 with no plugin 25 wp no print 19 wp print 19 Zarith 18
18. 43 CHAPTER 8 GENERAL KERNEL SERVICES Special Cases Modifications of options help verbose debug and their corresponding counterpart as well as quiet and unicode are not written in the journal 44 Chapter 9 Graphical User Interface Running frama c gui or frama c gui byte displays the Frama C Graphical User Interface GUI 9 1 Frama C Main Window Upon launching Frama C in graphical mode on some C files the following main window is displayed figure 9 1 Bora Toolbar Source file ere a home ftk Projects fc elements demo wp c A A s v home ftk Projects fc elements demo wp c predicate P int x 1 axiomatic A t f 2 predicate P int x 3 g 4 job Normalized source code view z e ensures rindo main ensures P result 7 PR ae anais A T e assigns nothing 8 r Original source code view extern int f int i A assigns nothing ge eaae Br extern int g int j 2 int g int j void job int t int A 12 void job int t int A 13 lt 100 File tree El E a En AAA 14 assert 50 lt A lt 100 io 15 O _ loop invariant 0 s in i s 50 7 SS ES o loop invariant Y Z k lt kak lt i P t k El 476 Woop Invariant 0 4 2228 3 o op assigna do Eat Ag 17 loop invariant forall integer k lt k lt i gt P t k E d 18 loop assigns i t 0 49 r 19 e while i lt 50 t i f i i 3 20 for int i 0
19. As for string options the extending format is also possible option_name values This last format must be used if your argument contains a minus sign you have to use it For instance you can ask the C preprocessor to search for header files in directory src by setting cpp extra args I src Categories are specific values which describe a subset of values Their names begin with an Available categories are option dependent but most set options accept the category all which define the set of all acceptable values For instance you can ask the Value plug in to use the ACSL specification of each functions but main instead of their definitions by setting val use spec all main If the first character of a set value is either O or it must be escaped with a Map Options Map options are set options whose values are of the form key value For instance you can override the default Value s slevel 7 for functions and g by setting slevel functions f 16 g 42 3 3 4 Splitting a Frama C Execution into Several Steps By default Frama C parses its command line in an unspecified order and runs its actions according to the read options To enforce an order of execution you have to use the option then Frama C parses its command line until the option then and runs its actions accord ingly then it parses its command line from this option to the end or to the next occurrence of then and runs its actions accor
20. C program see Section 5 3 ocode lt file name gt redirects all output code of the current project to the designated file keep comments keeps C comments in lined in the code unicode uses unicode characters in order to display some ACSL symbols This option is set by default so one usually uses the opposite option no unicode A series of dedicated options deal with the display of floating point and integer numbers float hex displays floating point numbers as hexadecimal float normal displays floating point numbers with an internal routine float relative displays intervals of floating point numbers as lower bound width big ints hex lt max gt print all integers greater than max in absolute value using hexadec imal notation 21 CHAPTER 3 GETTING STARTED 3 4 Environment Variables Different environment variables may be set to customize Frama C 3 4 1 Variable FRAMAC_LIB External plug ins see Section 4 3 or scripts see Section 4 4 are compiled against the Frama C compiled library The Frama C option print lib path prints the path to this library The default path to this library may be set when configuring Frama C by using the configure option libdir Once Frama C is installed you can also set the environment variable FRAMAC_LIB to change this path 3 4 2 Variable FRAMAC_PLUGIN Dynamic plug ins see Section 4 4 are searched for in a default directory The Frama C option print plugin p
21. Software Analyzers User Manual a Lust Frama C User Manual Release Sodium 20150201 Loic Correnson Pascal Cuoq Florent Kirchner Virgile Prevosto Armand Puccetti Julien Signoles and Boris Yakobowski CEA LIST Software Safety Laboratory Saclay F 91191 2009 2015 CEA LIST This work has been supported by the ANR project CAT ANR 05 RNTL 00301 and by the ANR project U3CAT 08 SEGI 021 01 CONTENTS Contents Foreword 9 1 Introduction 11 1 1 About this document a oaos 11 Co COLO cea e e A BAR A wae E O RO 11 2 Overview 13 21 Wheaties FOME e s pie ed Rk RRR A A a 13 2 2 Framal as a State Analysis Tool ooo Boe ek eg BR ee ae e 13 2 2 1 Frama C as a Lightweight Semantic Extractor Tool 14 2 2 2 Frama C for Formal Verification of Critical Software 14 2 3 Frama C as a Tool for C programs 0 00000 eae 14 2 4 Frama C as an Extensible Platform gt eo s coco e csocsi aor eme Kh oee 14 2 5 Frama C as a Collaborative Platform ooa e 15 2 6 Frama C as a Development Platformi aa va spa re 15 2 7 Frama C as an Educational Platform 16 3 Getting Started 17 Sol Instsllation ss ses 89 4 hao a el 17 3 2 One Framework Four Executables oaoa sa eaa a es 18 3 3 Frama C Command Line and General Options s sosoo 19 Sod rettme Help 2 0 00 wa saaa RR Ew RE RR e a ae A 19 diz Pemi Version ss dr do Ree ee ie 19 Soo Options Outlin
22. 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 51 Appendix A Changes This chapter summarizes the changes in this documentation between each Frama C release First we list changes of the last release Sodium 20150201 Normalizing the Source Code new options initialized padding locals and simplify trivial loops e Pre processing the Source Files new options cpp gnu like and frama c stdlib e Customizing Analyzers new options add symbolic path and permissive e Getting Started document options containing several values aka set and map e Getting Started improve documentation of options e Getting Started document new option then last Neon 20140 01 e Getting Started fixes list of requirements for compiling Frama C e Preparing the Sources new option agressive merging e General Kernel Services change the default name of the journal e Getting Started new options
23. alue it is assigned to if such a conversion is au thorized by C standard Otherwise a temporary variable separates the call and the cast The default is to have implicit casts for function calls so the opposite form no collapse call cast is more useful constfold performs a syntactic folding of constant expressions For instance the expres sion 1 2 is replaced by 3 continue annot error just emits a warning and discards the annotation when it fails to type check instead of generating an error errors in C are still fatal enums lt repr name gt specifies which representation should be used for a given enumerated type Namely C standard allows to use any integral types in which all the corresponding tags can be represented Default is gcc enums List of supported options can be obtained by typing frama c enums help This includes e int treat everything as int including enumerated types with packed attribute e gcc enums use an unsigned integer type when no tag has a negative value and choose the smallest rank possible starting from int default GCC s behavior e gcc short enums use an unsigned integer type when no tag has a negative value and choose the smallest rank possible starting from char GCC s fshortenums option force rl arg eval forces right to left evaluation order of function arguments C standard does not enforce any evaluation order and the default is thus to leave it unspecified initiali
24. ama 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 effectively 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 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 program analysis using Frama C as a testbed for your ideas is a choi
25. ama 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 necessary for normal use but it may be generated with the command make static External dynamic plug ins may be configured and compiled at the same time as the Frama C kernel by using the option enable external lt path to plugin gt This option may be passed several times 4 4 Loading Dynamic Plug ins At launch Frama C loads all dynamic plug ins it finds if the option dynlink is set That is the normal behavior you have to use its opposite form no dynlink in order not to not load any dynamic plug in When loading dynamic plug ins Frama C searches for them in directories indicated by frama c print plugin path see Section 3 4 2 Frama C can lo cate 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 any ex tension 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 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 warn
26. antical analysis at the first call to f since nothing would be known on the memory state afterwards The user is invited to check that the generated clause makes sense and to provide an explicit assigns clause if this is not the case The following options allow to customize the normalization process agressive merging forces some function definitions to be merged into a single function if they are equal modulo renaming Note that this option may merge two functions even if their original source code is different but their normalized version coincide This option is mostly useful to share function definitions that stems from headers included by several source files allow duplication allows the duplication of small blocks of code during normalization of loops and tests This is set by default and the option is mainly found in its opposite form no allow duplication which forces Frama C to use labels and gotos instead Note that bigger blocks and blocks with a non trivial control flow are never duplicated Option ulevel see below is not affected by this option and always duplicates the loop body 28 5 3 NORMALIZING THE SOURCE CODE 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 collapse call cast allows in some cases the value returned by a function call to be implicitly cast to the type of the v
27. ath prints the path to this directory It can be changed by setting the environment variable FRAMAC_PLUGIN 3 4 3 Variable FRAMAC SHARE Frama C looks for all its other data installed manuals configuration files C modelization libraries etc in a single directory The Frama C option print share path prints this path The default path to this library may be set when configuring Frama C by using the configure option datarootdir Once Frama C is installed you can also set the environment variable FRAMAC_SHARE to change this path A Frama C plug in may have its own share directory default is frama c print share path lt plug in shortname gt If the plug in is not installed in the standard way you can set this share directory by using the option lt plug in shortname gt share 3 4 4 Variable FRAMAC_SESSION Frama C may have to generate files depending on the project under analysis during a session in order to reuse them later in other sessions By default these files are generated or searched in the subdirectory frama c of the current directory You can also set the environment variable FRAMAC_SESSION or the option session to change this path Each Frama C plug in may have its own session directory default is frama c lt plug in shortname gt It is also possible to change a plug in session directory by using the option lt plug in shortname gt session 3 4 5 Variable FRAMAC_CONFIG Frama C may have to generat
28. atuses GL A Short Detour through Annotations cs eco ecos Pe a in 7 2 Properties and the Statuses Thereof 2 2 22 CE nenne 7 3 Consolidating Property Statuses ee ee General Kernel Services 8 1 Projects patas can ee Ge BA ee oe a eee en 31 1 Creatine Projects cs a eu sam Fined nd SA des ME a y 812 Using Projects cessam Kennen end 8 1 3 Saving and Loading Projects 8 2 Dependencies between Analyses 2 0 nenn 8 3 Jouknalsatlon ua a ee ee Re i d A Graphical User Interface 91 Frama C Main Winde s ce ioe os Br dew ee ee I Were DAE ae oa co th le ha fs ee A ee leet aa a E BEE asd a um ek ce oe ee ee ee we Be ee E 25 25 25 26 26 27 27 28 28 30 31 33 33 33 34 37 37 38 38 41 41 41 41 42 42 43 CONTENTS 10 Reporting Errors A Changes Bibliography List of Figures Index 59 61 Foreword This is the user manual of Frama C The content of this document corresponds to the version Sodium 20150201 March 5 2015 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 Benjamin Monate and Dillon Pariente Inttp frama c com Chapter 1 Introduction This is Frama C s user manual Frama C is an open sou
29. cation 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 documents 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 by code review 2 3 Frama C as a Tool for C programs The C source code analyzed by Frama C 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 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 organized into a modular 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 which provides common functionalities and collaborative data structures 14 2 5 FRAMA C AS A COLLABORATIVE PLATFORM Several ready to use analyses are included in the Frama C distribution This
30. ce 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 15 CHAPTER 2 OVERVIEW orthogonal to those you want to consider in particular the Value Analysis provides sets of 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 Development Guide 12 2 7 Frama C as an Educational Platform Frama C is already being used as parts of courses on formal verification program specification testing static analysis and abstract interpretation with audiences ranging from Master s students to active professionals in institutions world wide Frama C is part of the curriculum at several universities in France England Germany Portugal Russia and in the US at schools such as Ecole Polytechnique ENSIIE ENSMA or ENSI Bourges and as part of continuing education units at CNAM or at Fraunhofer FIRST If you are a teacher in the extended field of software safety using Frama C as a support for your course and lab work is a choice to consider You may benefit from a clean focused interface a choice of techniques to illustrate and a in tool pedagogical presentation of their abstract values at all program points A number of course materials are
31. ctive the original one is not The plug ins view shows specific plug in interfaces The interface of each plug in can be collapsed The messages view contains by default four different pages namely the Information page which provides brief details on the currently selected object or informative messages from the plugins the Messages page shows most important messages especially all alarms that the Frama C kernel or plug ins generate Please refer to the specific documentation of each plug in in order to get the exact form of alarms Alarms that have a location in the original source can be double clicked this location will then be shown in the original and normalized source code viewers Beware that alarms are not stored in batch mode to reduce memory consumption the Messages panel will remain empty if the GUI loads a file saved in batch mode see Section 8 1 3 If you want to store these alarms in batch mode use the option collect messages the Console page displays messages to users in a textual way This is the very same output than the one shown in batch mode the Properties page displays the local and consolidated statuses of properties Notice however that the location in the normalized source may not perfectly correspond as more than one normalized statement can correspond to a source location 46 9 2 MENU BAR 9 2 Menu Bar The menu bar is organised as follows The file
32. d Computing SAC pages 1230 1235 ACM March 2013 Philippe Herrmann and Julien Signoles Annotation Generation Frama C s RTE plug in April 2013 http frama c com download frama c rte manual pdf Florent Kirchner Nikolai Kosmatov Virgile Prevosto Julien Signoles and Boris Yakobowski Frama c A software analysis perspective Formal Aspects of Computing pages 1 37 2015 Extended version of 6 Julien Signoles Frama C s E ACSL Plug in February 2015 http frama c com eacsl Julien Signoles Loic Correnson Matthieu Lemerre and Virgile Prevosto Frama C Plug in Development Guide February 2015 http frama c cea fr download plugin developer pdf 57 LIST OF FIGURES List of Figures dd Initial View 2 224 pise a 845 sa a A a O Se OD G 45 9 2 The Analysis Configuration Window 2 2 0020004 47 10 1 The BIS Bugs Reporting Page 2 6g ae asa alia a ara aaa 50 59 absolute valid range 34 42 43 ACSL 14 15 21 27 29 37 38 add path 26 add symbolic path 34 agressive merging 28 allow duplication 28 annot 29 Batch version 18 big ints hex 21 Bytecode 18 C compiler 17 C pre processor 17 C99 ISO standard 14 collapse call cast 29 collect messages 46 config 23 constfold 29 continue annot error 28 29 cpp command 27 cpp extra args 19 27 cpp gnu like 27 28 datarootdir 22 debug 21 42 44 dynlink 26 enable externa
33. d cp 1 2 file1 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 If you use the above option you may use the option cpp gnu like to indicate that the custom preprocessor accepts the same set of options as GNU cpp 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 using GCC as pre processor and putting the option pp annot on the Frama C command line Note that ACSL annotations are pre processed separately from the C code and that argu ments given as cpp extra args are not given to the second pass of pre processing Instead pp annot relies on the ability of GCC to output all macros definitions including those given with D in the pre processed file In particular cpp extra args must be used if you are 27 CHAPTER 5 PREPARING THE SOURCES including header files who behave differently depending on the number of times they are included An experimental incomplete specific C standard library is bundled with Frama C and in stalled in the sub directory libc of the directory D printed by frama c print share path It contains standard C headers some ACSL specifications and definitions for some li brary functions To use these headers instead of the standard library ones the option frama c stdlib set by default adds
34. ding to the read options Note that this second run starts with the results of the first one Consider for instance the following command frama c val ulevel 4 file c then ulevel 5 It first runs the value analysis plug in option val 7 with an unrolling level of 4 option ulevel Section 5 3 Then it re runs the value analysis plug in option val is still set with an unrolling level of 5 It is also possible to specify a project see Section 8 1 on which the actions applied thanks to the option then on Consider for instance the following command frama c semantic const fold main file c then on propagated val It first propagates constants in function main of file c option semantic const fold which generates a new project called propagated Then it runs the value analysis plug in on this new project The last possibility is the option then last which applies the next actions on the last project created by a program transformer For instance the following command is equivalent to the previous one frama c semantic const fold main file c then last val 20 3 3 FRAMA C COMMAND LINE AND GENERAL OPTIONS 3 3 5 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 it to O limits the output to warnings and error messages
35. e zu s gora de wur Kane a en 19 3 3 4 Splitting a Frama C Execution into Several Steps 3 3 5 Verbosity and Debugging Levels 33 8 Cetta time vale eek ek RA a ae 3 3 7 Inputs and Outputs of Source Code 34 Environment Variables us caia en me DR GUS es 3411 Variable FRAMAC LIB 2 u wu ae an ars gr Edo m a Ee go CONTENTS 3 4 2 Variable FRAMAC_PLUGIN 2 0 SS Variable FRAMAE SHARE iu dor e aa O44 Variable PRAMAC SESSION gt ar a Ra a AA 3 4 5 Variable FRAMAC CONFIG s o accses aanrada an aaiae da Ex AUS cidad Re ee eS Setting Up Plug ins 4 1 The Plaga TAXONOMY lt a o c ann aaa mn de ede ee ee ar 4 2 Installing Internal Plug ins i e sca ssar ena osi eaa sekaa aa 4 3 Installing External Plug ins 2 2 2 CL EEE nn 44 Leading Dynaniie Plus c e e ua He Be Hr rn a in Preparing the Sources 5 1 Preprocessing the Source Files co e coc 206 3 Sins a en eh wel 5 2 Merging the Source Code files s ss s se eos s ro sma da 5 3 Normalizing the Source Code 2 2 Em Ener 5 4 Warnings during normalization s so oi sgoe poaa nn 5 5 Testing the Source Code Preparation ea e e Platform wide Analysis Options 6 1 Entry Pombo 2 2004 04482 RR EAS we ED eee RD ee k G 6 2 Feedback Options 2 aca a 648544 De Sb ea ee kee A ee 63 Customizing Analyzers o sos Ge Ae bee die ee Pe ee ne in Property St
36. e configuration files during a session in order to reuse them later in other sessions 22 3 5 EXIT STATUS By default these files are generated or searched in a subdirectory frama c or frama c of the system s default configuration directory e g USERPROFILE on Windows or HOME config on Linux You can also set the environment variable FRAMAC_CONFIG or the option config to change this path Each Frama C plug in may have its own configuration directory if required on Linux default is HOME config frama c lt plug in shortname gt It is also possible to change a plug in s config directory by using the option lt plug in shortname gt config 3 5 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 of invalid user input 2 Frama C exits because the user kills it usually via Ctrl C 3 Frama C exits because the user tries to use an unimplemented feature Please report a feature request on the Bug Tracking System see Chapter 10 4 5 6 Frama C exits on an internal error Please report a bug report on the Bug Tracking System see Chapter 10 125 Frama C exits abnormally on an unknown error Please report a bug report on the Bug Tracking System see Chapter 10 23 Chapter 4 Setting Up Plug ins The Frama C platform has been designed to support third party plug ins In the present chapter we present
37. efault 35 Chapter 7 Property Statuses This chapter touches on the topic of program properties and their validation by either standalone or cooperating Frama C plug ins The theoretical foundation of this chapter is described in a research paper 5 7 1 A Short Detour through Annotations Frama C supports writing code annotations with the ACSL language 2 The purpose of annotations is to formally specify the properties of C code Frama C plug ins can rely on them to demonstrate that an implementation respects its specification Annotations can originate from a number of different sources the user who writes his own annotations an engineer writing code specifications is the prevalent scenario here some plug ins may generate code annotations These annotations can for instance indi cate that a variable needs to be within a safe range to guarantee no runtime errors are triggered cf the RTE plug in 9 the kernel of Frama C that attempts to generate as precise an annotation as it can when none is present Of particular interest is the case of unannotated function prototypes the ACSL specification states that a construct of that kind potentially modifies everything 2 Sec 2 3 5 For the sake of precision and conciseness the Frama C kernel breaks this specification and generates a function contract with clauses that relate its formal parameters to its results This behavior might be incorrect
38. es or behaves abnormally you are invited to bug report v a the Frama C Bugs Tracking System BTS located at http bts frama c com Opening a BTS account is required for such a task Bug reports can be marked as public or private Public bug reports can be read by anyone and are indexed by search engines Private bug reports are only shown to Frama C developers Reporting a new issue opens a webpage similar to the one shown in Figure 10 1 This page also has a link to an advanced bugs reporting page that allows you 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 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 with 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 be
39. f floating point numbers e Preparing the sources document generation of assigns clause for function proto types without body and proper specification e Property Statuses new chapter to document property statuses e GUI document new interface elements Carbon 20110201 e Getting Started exit status 5 is now 127 new exit status 5 and 6 e GUI document new options collect messages 54 Carbon 20101201 e Getting Started document new options then and then on e Getting Started option obfuscate is no more a kernel option since the obfuscator is now a plug in Boron 20100401 e Preparing the Sources document usage of the C standard library delivered with Frama C e Graphical User Interface simplified and updated according to the new implemen tation e Getting Started document environment variables altogether e Getting Started document all the ways to getting help e Getting Started OcamlGraph 1 4 instead 1 3 will be used if previously installed e Getting Started GtkSourceView 2 x instead of 1 x is now required for building the GUI e Getting Started documentation of the option float digits Preparing the Sources documentation of the option continue annot error e Using plug ins new option dynlink e Journalisation a journal is generated only whenever Frama C crashes on the GUI e Configure new option with no plugin e Configure option with all static set by default when native dynamic l
40. fic options 6 1 Entry Point The following options define the entry point of the program and related initial conditions main lt function_name gt specifies that all analyzers should treat 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 Feedback Options All Frama C plug ins define the following set of common options lt plug in shortname gt help or lt plug in shortname gt h prints out the list of options of the given plug in lt plug in shortname gt verbose lt n gt sets the level of verbosity to some positive integer n A value of O means no information messages Default is 1 lt plug in shortname 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 0 no debugging message lt plug in shortname gt msg key lt keys gt sets the categories of messages that must be out put for the plugin keys is a comma separated list of names The list of available categories can be obtained with lt plug in shortname gt msg key help
41. haviour 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 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 8 3 Beware that this journal does not replace nor contain the input files that must be added to the bug report too see below French is also a possible language choice for private entries 2You can also have a look at the associated Frama C wiki http bts frama c com dokuwiki doku php id mantis frama c start 49 CHAPTER 10 REPORTING ERRORS 2009 09 15 16 18 CEST Project Frame c x Switch select have not tried E check to report more issues Mantis 1 1 6 7 Copyright 2000 2008 Mantis Group Figure 10 1 The BTS Bugs Reporting Page 50 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 C source files shell scripts to run Frama C with your options and environment
42. here to This 13 CHAPTER 2 OVERVIEW of course requires more work from the user than heuristic bug finding tools usually do but some 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 results about complex semantic properties 2 2 1 Frama C as a Lightweight Semantic Extractor Tool Frama C analyzers by offering the possibility to extract semantic information from C code can help better understand a program source 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 can verify that an implementation complies with a related set of formal specifications Specifications are written in a dedicated language ACSL ANSI ISO C Specifi
43. id in C90 or in C99 but could be valid K amp R code Option no warn undeclared callee disables this warning Beware that parsing is still not guaranteed to succeed regardless of the emission of the warning Upon encountering a call to an undeclared function Frama C attempts to continue its parsing phase by inferring a prototype corresponding to the type of the arguments at the call modulo default argument promotions If the real declaration does not match the inferred prototype parsing will later end with an error 30 5 5 TESTING THE SOURCE CODE PREPARATION 5 5 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 frama c lt input files gt If you need to use other 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 31 Chapter 6 Platform wide Analysis Options The options described in this chapter provide each analysis with common hypotheses that influence directly their behavior For this reason the user must understand them and the interpretation the relevant plug ins have of them Please refer to individual plug in docu mentations e g 7 3 4 for speci
44. implifies trivial loops such as do while 0 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 7 Below is a typical example of use loop pragma UNROLL 10 x for i 0 i lt 9 i The transformation introduces an UNROLL pragma indicating that the unrolling process has been done loop unrolled 10 times loop pragma UNROLL 10 loop pragma UNROLL done 10 x remaining loop That allows to disable unrolling transformation on such a loop when reusing Frama C with a code obtained by a previous use of Frama C tool To ignore this disabling UNROLL pragma and force unrolling the option ulevel force has to be set Passing a negative argument to ulevel will disable unrolling even in case of UNROLL pragma 5 4 Warnings during normalization Two options can be used to influence the warnings that are emitted by Frama C during the normalization phase warn decimal float lt freq gt warns when floating point constants in the program cannot be exactly represented freq must be one of none once or all Defaults to once warn undeclared callee emits a warning each time a call to a function that has not been declared previously is found This is inval
45. in different functions unspecified access does not detect that warn signed downcast may be used to check that the analyzed code does not downcast an integer to a signed integer type This option is not set by default Without it the analyzers do not perform such a verification For instance consider the following function short truncate int n 4 return short n If warn signed downcast is set analyzers detect an error on short n which down casts a signed integer to a signed short Without it no error is detected warn unsigned downcast is the same as warn signed downcast for downcasts to un signed integers This option is also not set by default warn signed overflow may be used to check that the analyzed code does not overflow on integer operations If the opposite option no warn signed overflow is specified the analyzers assume that operations over signed integers may overflow by following two s complement representation This option is set by default For instance consider the function abs that computes the absolute value of its int argument int abs int x if x lt 0 x x return x By default analyzers detect an error on x since this operation overflows when MININT is the argument of the function But with the no warn signed overflow option no error is detected warn unsigned overflow is the same as warn signed overflow for operations over un signed integers This option is not set by d
46. ing will be emitted at launch if this is not the case The load script option requires the OCaml compiler that was used to compile Frama C to be available and the Frama C compiled library to be found see Section 3 4 1 With the extension exe on Windows OS 26 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 analyze must be provided on the command line or chosen interactively in the GUI Files with the suffix i 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 2 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 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 filei c file2 i frama c cpp comman
47. 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 finding 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 ad
48. l 26 enums 29 float hex 21 float normal 21 float relative 21 force rl arg eval 29 frama c 18 frama c gui 18 45 frama c gui byte 18 45 frama c stdlib 28 frama c byte 18 FRAMAC_CONFIG 23 FRAMAC_LIB 22 INDEX Index FRAMAC_PLUGIN 22 FRAMAC_SESSION 22 FRAMAC_SHARE 22 GTK 18 GtkSourceView 18 h 19 help 19 42 44 help 19 initialized padding locals 29 Installation 17 Interactive version 18 Journal 43 journal disable 19 43 journal enable 19 43 journal name 43 keep comments 21 keep switch 29 keep unused specified functions 29 kernel debug 21 kernel h 19 kernel help 19 kernel verbose 21 Lablgtk 18 lib entry 33 libdir 22 load 42 42 43 46 load module 26 48 load script 26 43 48 machdep 29 main 33 Native compiled 17 18 no unicode 19 OCaml compiler 17 OcamlGraph 18 ocode 21 Options 19 permissive 34 Plug in Dynamic 25 26 48 External 25 26 Internal 25 25 Static 25 26 pp annot 27 Pragma UNROLL 30 print 21 28 print lib path 22 26 print plugin path 22 26 print share path 22 26 Project 41 quiet 21 42 44 remove unused specified functions 29 safe arrays 34 save 42 42 43 46 semantic const fold 20 session 22 simplify cfg 30 simplify trivial loops 30 slevel functions 20 then 20 then last 20 then on 20 41 time 21 type check 3
49. lute valid range see Section 6 3 Just after Frama C saves the results on file foo sav and exists At loading time 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 absolute valid range 0 0x1000 val foo c frama c load foo sav absolute valid range 0 0x2000 The first command produces the very same result than above However in the second load command Frama C knows that one parameter has changed Thus it discards the saved results of the value analysis and recomputes it on the same source code by using the parameters ulevel 5 absolute valid range 0 0x2000 and the default value of each other parameter In the same fashion results from an analysis A may well depend on results from another analysis Aa Whenever the results from Aa change Frama C automatically discards results from A For instance slicing results depend on value analysis results thus the slicing results are discarded whenever the value analysis ones are 8 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 SESSION_DIR frama_c_journal ml where SESSION_DIR is the Frama C session directory see Section 3 4 4
50. m by preserving a specified behaviour 8 1 2 Using Projects The list of existing projects of a given session is visible in the graphical mode through the Project menu see Section 9 2 Among other actions on projects duplicating renaming removing saving etc this menu allows the user to switch between different projects during the same session In batch mode the only way to handle a multi project session is through the command line option then on see Section 3 3 4 41 CHAPTER 8 GENERAL KERNEL SERVICES 8 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 In case of a fatal error or an unexpected error saving is done as well but the generated file is modified into file crash since it may have been corrupted In other error cases no saving is done The same operations are available through the GUI 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 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 explicitly set in the current session Consider for instance the f
51. mands Chapter 4 explains the basics of plug in categories installation and usage Chapter 5 presents the options of the source code pre processor Chapter 6 gives some general options for parameterizing analyzers 11 CHAPTER 1 INTRODUCTION Chapter 7 touches on the topic of code properties and their validation by the platform Chapter 8 introduces the general services offered by the platform Chapter 9 gives a detailed description of the graphical user interface of Frama C Chapter 10 explains how to report errors via the Frama C s Bug Tracking System 12 Chapter 2 Overview 2 1 What is Frama C Frama C is a platform dedicated to the analysis of source code written in C The Frama C platform gathers several analysis techniques into a single collaborative extensible framework The collaborative approach of Frama C allows analyzers to build upon the results already computed by other analyzers in the framework Thanks to this approach Frama C can provide a number of sophisticated tools such as a slicer 3 and a dependency analyzer 7 Chap 6 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
52. oading is not available Beryllium 20090902 e First public release 55 BIBLIOGRAPHY Bibliography 1 Patrick Baudin Pascal Cuoq Jean Christophe Filli tre Claude Marche Benjamin 10 11 12 Monate Yannick Moy and Virgile Prevosto ACSL ANSI ISO C Specification Lan guage Version 1 8 Frama C Oxygen implementation March 2014 Patrick Baudin Jean Christophe Filli tre Claude Marche Benjamin Monate Yannick Moy and Virgile Prevosto ACSL ANSI ISO C Specification Language Version 1 8 March 2014 Patrick Baudin and Anne Pacalet Slicing plug in http frama c com slicing html Loic Correnson Zaynah Dargaye and Anne Pacalet Frama C s WP plug in February 2015 http frama c com download frama c wp manual pdf Loic Correnson and Julien Signoles Combining Analysis for C Program Verification In Formal Methods for Industrial Critical Systems FMICS 2012 Pascal Cuoq Florent Kirchner Nikolai Kosmatov Virgile Prevosto Julien Signoles and Boris Yakobowski Frama C A software Analysis Perspective In Software Engineering and Formal Methods SEFM October 2012 Pascal Cuoq Boris Yakobowski and Virgile Prevosto Frama C s value analysis plug in February 2015 http frama c cea fr download value analysis pdf M Delahaye N Kosmatov and J Signoles Common specification language for static and dynamic analysis of C programs In the 28th Annual ACM Symposium on Applie
53. ollowing 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 Recommendation 8 1 Saving the result of a time consuming analysis before trying to use it in different settings is usually a good idea Beware that all the existing projects are deleted even if an error occurs when reading the file We strongly recommend you to save the existing projects before loading another project file Special Cases Options help verbose debug and their corresponding counterpart as well as quiet and unicode are not saved on disk 8 2 Dependencies between Analyses Usually analyses do have parameters see Chapter 6 Whenever the values of these parame ters change the results of the analyses may also change In order to avoid displaying results that are inconsistent with 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 absolute valid range 0 0x1000 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 option ulevel see Section 5 3 To compute its result the value analysis assumes the 42 8 3 JOURNALISATION memory range 0 0x1000 is addressable option abso
54. orcing the compilation and installation of a plug in against configure s autodetection based default may cause the entire Frama C configuration to fail You can also use the option with no plugin in order to disable all plug ins 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 This option is set by default on systems that do not support native dynamic loading 25 CHAPTER 4 SETTING UP PLUG INS 4 3 Installing External Plug ins To install an external plug in Frama C itself must be properly installed first In particu lar frama c print share path and must return the share directory of Frama C see Sec tion 3 4 3 while frama c print lib path must return the directory where the Frama C compiled library is installed see Section 3 4 1 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 automati cally generated when an external plug in is compiled This executable contains the Fr
55. r Shttp forge ocamlcore org projects zarith On Windows OS the usual extension exe is added to each file name For a single analysis project Multiple projects can only be handled in the interactive version or program matically See Section 8 1 18 3 3 FRAMA C COMMAND LINE AND GENERAL OPTIONS 3 3 Frama C Command Line and General Options 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 either the option kernel help or kernel h The options of a plug in are displayed by using either the option lt plug in shortname gt help or lt plug in shortname gt h Furthermore either the option help or h or help lists all available plug ins and their short names 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 Options Outline 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 anal ysis interactively the command frama c gui val foo c can be used to launch the value analysis on the file foo c and
56. rce platform dedicated to the analysis of source code written in the C programming language The Frama C platform gathers several 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 the use of the analyzers provided in the Frama C distribution Value Analysis Slicing Each of these analyses has its own specific documentation 7 Further more a research paper 6 10 gives a synthetic view of the platform its main and composite analyses and some of its industrial achievements while the development of new analyzers is described in the Plug in Development Guide 12 1 1 About this document Appendix A references all the changes made to this document between successive Frama C releases In the index page numbers written in bold italics e g 1 reference the defining sections for the corresponding entries while other numbers e g 1 are less important references The most important paragraphs are displayed inside gray boxes like this one A plug in developer must follow them very carefully 1 2 Outline 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 of installation and com
57. ries here The file tree provides a tree like structure of the source files involved in the current analysis This tree lists all the global variables and functions each file contains Within a file entries are sorted alphabetically without taking capitalization into account Functions are underlined to separate them from variables Plug ins may also display specific information for each file and or function Finally the Source file button offers some options to filter the elements of the file tree e The Hide variables and Hide functions options offer the possibility to hide the non desired entries from the tree e The Flat mode option flattens the tree by removing the filename level Instead functions and globals are displayed together as if they were in a big namespace This makes it easier to find a function whose only the name is known The normalized and original source code views display the source code of the current selected element of the file tree and its normalized code see Section 5 3 Left clicking on an object statement left value etc in the normalized source code view displays information about it in the Information page of the Messages View and displays the corresponding object of the original source view while right clicking on them opens a contextual menu Items of this menu depend on the kind of the selected object and on plug in availability Only the normalized source view is intera
58. semantic constant folding gt slicing gt sparecode gt syntactic callgraph gt users gt value analysis Cancel Execute Figure 9 2 The Analysis Configuration Window 47 CHAPTER 9 GRAPHICAL USER INTERFACE e Item Compile and run an ocaml script allows you to run an OCaml file as a dynamic plug in in a way similar to the option load script see Section 4 4 e Item Load and run an ocaml module allows you to run a pre compiled OCaml file as a dynamic plug in in a way similar to the option load module see Sec tion 4 4 e Other items are plug in specific The debug menu is only visible in debugging mode and provides access to tools for helping to debug Frama C and their plug ins The help menu provides help items 9 3 Tool Bar The tool bar offers a more accessible access to some frequently used functions of the menu bar Currently the available buttons are from left to right e The Quit button that exits Frama C e Four buttons New session Reparse Load Session and Save session equivalent to the corresponding entries in the File menu e Two navigation buttons Back and Forward They can be used to move within the history of the functions that have been viewed e The Analyses button equivalent to the one in the Analyses menu e A Stop button which halts the running analyses and restores Frama C in its latest valid configuration 48 Chapter 10 Reporting Errors If Frama C crash
59. t 2147483647 at a program point 7 A trace where pli 46341 at will invalidate this property and will stop short of reaching any instruction succeeding 7 An important part of the interactions between Frama C components the plug ins the kernel rely on their capacity to emit a judgment on the validity of a property P at program point i In Frama C nomenclature this judgment is called a local property status The first part of a local status ranges over the following values e True when the property is true for all traces e False when there exists a trace that falsifies the property e Maybe when the emitter e cannot decide the status of P As a second part of a local property status an emitter can add a list of dependencies which is the set of properties whose validity may be necessary to establish the judgment For instance when the WP plug in 4 provides a demonstration of a Hoare triple A c B it starts by setting the status of B to True and then adds to this status a dependency on property A In more formal terms it corresponds to the judgment F A gt B for a trace to be valid in B it may be necessary for A to hold This information on the conditional validity of B is provided as a guide for validation engineers and should not be mistaken for the formal proof of B which only holds when all program properties are verified hence the local status 7 3 Consolidating Property Statuses Recall our previo
60. t there are unknown or never_tried there is no certainty with regards to any other status including surely_valid properties These consolidated statuses are displayed in the GUI see section 9 for details or in batch mode by the report plug in 40 Chapter 8 General Kernel Services This chapter presents some important services offered by the Frama C platform 8 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 an 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 8 1 1 Creating Projects A new project is created in the following cases e at initialization time a default project is created or e via an explicit user action in the GUI 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 A typical example is code slicing which tries to simplify a progra
61. us example where the WP plug in sets the local status of a property B to True with a dependency on a property A This might help another plug in decide that the validity of a third property C that hinges upon B now depends on A When at last A is proven by say the value analysis plug in the cooperative proofs of A B and C are marked 1Some plug ins might consider all possible traces which constitute a safe over approximation of the intended property 38 7 3 CONSOLIDATING PROPERTY STATUSES as completed In formal terms Frama C has combined the judgments FA gt B FB C and A into proofs of Band F C by using the equivalent of a modus ponens inference HA FASB HB Notice how without the final F A judgment both proofs would be incomplete This short example illustrates how incremental the construction of program property proofs can be By consolidating property statuses into an easily readable display Frama C aims at informing its users of the progress of this process allowing them to track unresolved dependencies and selectively validate subsets of the program s properties As a result a consolidated property status can either be a simple status O never_tried when no status is available for the property unknown whenever the status is Maybe O surely valid when the status is True and dependencies have the consolidated status surely valid or considered valid O surely invalid when the
62. zed padding locals forces to initialize padding bits of locals to 0 If false padding bits are left uninitialized This option is set by default keep switch preserves switch statements in the source code Without this option they are transformed into if statements An experimental plug in may forget 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 keep unused specified functions does not remove from the AST uncalled function prototypes that have ACSL contracts This option is set by default So you mostly use the opposite form namely remove unused specified functions 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 compi lation parameters The machdep option provides a way to define all these parameters consistently in a single step The list of supported platforms can be obtained by typing 29 CHAPTER 5 PREPARING THE SOURCES frama c machdep help simplify cfg allows Frama C to remove break 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 simplify trivial loops s

User Manual - Frama-C

Contents

Download Pdf Manuals

Related Search

Related Contents