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] Analyzing ext2 source code with frama-c

  • Subject: [Frama-c-discuss] Analyzing ext2 source code with frama-c
  • From: dmentre at linux-france.org (David MENTRÉ)
  • Date: Thu, 17 Nov 2016 21:26:14 +0100
  • In-reply-to: <CA+m8BZoWu-HYyJe_Cu0-S9J+Mk4Mfv-NjFb5xmXh=SbL0PfrZw@mail.gmail.com>
  • References: <CA+m8BZoWu-HYyJe_Cu0-S9J+Mk4Mfv-NjFb5xmXh=SbL0PfrZw@mail.gmail.com>
Hello,

Le 2016-11-17 à 08:48, mohsen zandie a écrit :
> When i want to analyze some file in ext2 directory like acl.c with the
> following command in linux4.8.7 source code directory::
> ./../FramaC/frama-c-Aluminium-20160502/bin/frama-c -val
> -cpp-extra-args="-I include" fs/ext2/acl.c
>  
> I got fatal error which means i cant correctly set the value to find
> header file like asm/types.h
> 
> I don't even know how to set options for getting proper result for my
> purpose.

Beyond excellent answer of André, I would recommend to do the analysis
in several steps:

 1. Call just Frama-C on the source code (i.e. without -val option) to
be sure the C code is correctly understood by Frama-C;

 2. Add -val option. As your are analyzing big code, you'll probably
need to analyze parts separately, so use -lib-entry and use an
appropriate driver (to see an example of driver, look at a previous
message on this list:
https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-November/005169.html)

 3. Try to understand why you have so many alarms. Most of the time, it
is due to Value analysis doing over-approximations. You need to guess
what Value analysis is doing (use the information its provides,
especially value determined at specific point or path in the code) and
understand what the code is doing;

 4. Use -slevel-function option to tweak slevel to increase precision at
the relevant part in the code;

 5. Loop to step 2 until you are satisfied by the analysis.

Linux source code is complex. If you have never used Value analysis
before, I would recommend to start with simpler source code. Or at
least, focus on simplest parts of the source ext2 code.

Good luck and keep us informed of your results, you have an interesting
research subject.

Best regards,
david