--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Analyzing ext2 source code with frama-c



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>