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] Dead code that shouldn't be

  • Subject: [Frama-c-discuss] Dead code that shouldn't be
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Fri, 12 Dec 2008 11:07:34 +0100
  • In-reply-to: <1229048757.13603.14.camel@residence.localdomain>
  • References: <1229048757.13603.14.camel@residence.localdomain>
On Dec 12, 2008, at 3:25 AM, Jonathan-Christofer Demay wrote:

> I'm trying to analyze nullhttpd 0.5.0 (it's quite old, can get it  
> here:
> http://ftp.heanet.ie/disk1/sourceforge/n/nu/nullhttpd/nullhttpd-0.5.0.tar.gz) 
>  with frama-c. When I'm runnning the value dependencies plugin,  
> almost all the source code is marked as dead code.

This is what happens when a missing bit of context makes the
analyzer believe that a run-time error certainly happens quickly.

The analyzer tries to reduce the number of alarms
by removing (as best it can) the offending values from the
state it propagates, and it may end up with no possible values
left to propagate.
Because it forces itself to manipulate only supersets of
possible values, what you are describing can not be caused by
approximations in the analyzer. It is caused by wrong hypotheses.
That's good news because wrong hypotheses can be fixed.

One way to locate the instruction where it wrongly thinks that
a run-time error certainly happens is to follow the control flow
until the first dead statement in the gui. You can inspect the
values inferred by the analysis for variables, and even expressions,
just before that point to get an idea of why it thinks so.

> I must be missing something, but don't know exactly what, for now I'm
> using frama-c like this:
> cd ./nullhttpd-0.5.0/src
> frama-c-gui -val *.c


Even moving win32.c out of the way,
CIL refuses to link on my non-linux platform.
I get warnings such as:

Parsing
[preprocessing] running gcc -C -E -I.   server.c
old type = int (int  , int  , off_t  , off_t * , struct sf_hdtr * ,  
int  )

new type = int (int sid , unsigned char *file )

main.h:244: Error: Declaration of sendfile does not match previous  
declaration from /usr/include/sys/socket.h:582 (different number of  
arguments).
old type = int (pid_t _pid )

new type = int (void)

main.h:264: Error: Declaration of getsid does not match previous  
declaration from /usr/include/unistd.h:459 (different number of  
arguments).
[preprocessing] running gcc -C -E -I.   main.c
old type = int (int  , int  , off_t  , off_t * , struct sf_hdtr * ,  
int  )

new type = int (int sid , unsigned char *file )

would it be possible for you to make a self-contained analysis
project that contained all the headers used by the C files and
to post it somewhere?

Frama-C does not need to execute the code, so it is fine to analyze
a linux program on any other platform, but the headers must be
provided even if (on a Linux platform) they are in the system  
directories.

Pascal


-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081212/027d3026/attachment.htm