--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] First time with Frama-C



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é