--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2016 ---
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