--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2017 ---
Hello, Le 2017-02-03 à 07:53, Prithvi Raj Narendra a écrit : > I came across it in my search for a static analyser for the embedded > projects that I work on. Which kind of Analysis do you want to do with Frama-C? Frama-C is not a simple tool to which you input your source files and replies back a nice report to you. Frama-C is more like a toolbox, with lot of tools that you need learn and combine to reach your analysis objectives. If you don't know what to analyze, I recommend that you start with Value Analysis plug-in. Read its manual first! > My first issue is that with the GUI I'm not able to add any source > files. Usually I give all the C source files on the command line, something like: frama-c-gui <needed command line options> file1.c file2.c ... Most of the time, you'll need to use appropriate options to properly find and parse your header files. > I use arm gcc as the compiler. As usual the sequence is creating > dependencies and object files for every .c file and then linking them > (the command line for this is pasted below). How can I run Frama-C with > command line so that > 1. the libc library of ARM GCC, Frama-C is doing analysis (well more exactly some of its plug-ins) on C *source code*. So it does not matter which exact target is used, especially regarding libraries and so on. The only things that matter is the precise definition of your target platform regarding C types and endianess, i.e. big or little endian, size of int, short, long, etc. I would start with default definition for x86(_64?) platform and then tweak those parameters once you are comfortable with the use of the tool. > 2. since there is an extern variable that is used in a bit of assembly > code, a single c source file complains of undefined reference. Frama-C plug-ins cannot analyze assembly code. You'll have to write some C code or ACSL contracts to be able to analyze those parts of your code. You have a lot of documentation available. Read it! For example look at: * Available PDFs: http://frama-c.com/download.html * Frama-C blog: http://blog.frama-c.com/ There is a series of 3 parts on using Value Analysis starting here: http://blog.frama-c.com/index.php?post/2016/09/23/mini-acsl-tutorial Sincerely yours, D. Mentré