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: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Thu, 17 Nov 2016 19:45:27 +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,

A general technique that works in most cases is to modify the build 
process to produce preprocessed files (.i). For instance, with GCC/Clang 
this can be done by adding -E to the parsing command-line. This way, 
most compilation rules can be reused with minimal modifications.

Note, however, that Frama-C does not work with separate compilation: it 
requires all source files to be parsed at the same time, so if the build 
process has several commands for separate compilation, the user must 
combine them manually.

Also, Frama-C includes by default files from its own standard library, 
which is known to be incompatible with some standard headers, especially 
from large code bases, so adding -no-frama-c-stdlib might help avoid 
errors. The drawback is that then you will not have access to Frama-C 
annotations for some functions. Also, you may have to add something like 
"-I/usr/include" to include your own system's headers.

Overall, this process is not straightforward and depends on several 
factors, so some familiarity with the C compilation chain is necessary.

Finally, please consider providing more information about errors in the 
future, to help us reproduce and diagnose them.

Best regards,
André


On 17/11/2016 08:48, mohsen zandie wrote:
>
> Hi
>
> For an academic research i want to analyze Linux ext2 file system to 
> find bug like null pointer exception and any bug which lead to error 
> in file system.
> Can you help me how to analyze the ext2 source code?
>
> 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.
>
> I would be grateful if you give me some hint to accelerate my research.
> regards.
> Mohsen
>
>
> -- 
> ===================================
> Mohsen Zandieh
> Msc Student
> Department of Computer Engineering
> Sharif University of Technology
> ===================================
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Ingénieur-chercheur CEA/LIST
Laboratoire Sûreté et Sécurité des Logiciels

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161117/21f2e728/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161117/21f2e728/attachment.bin>