Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] First time with Frama-C
  • From: dmentre at linux-france.org (David MENTRÉ)
  • Date: Fri, 3 Feb 2017 08:21:36 +0100
  • In-reply-to: <CALu-FW04tRVNo9Amki=T2YbkN6qJRcPyAiGgFQLtmM1dQ_fQtw@mail.gmail.com>
  • References: <CALu-FW04tRVNo9Amki=T2YbkN6qJRcPyAiGgFQLtmM1dQ_fQtw@mail.gmail.com>
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é