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 (CUOQ Pascal)
  • Date: Sat, 13 Dec 2008 13:43:06 +0100
  • References: <1229048757.13603.14.camel@residence.localdomain><A113C951-6B87-48B8-960F-7EAF4370B1B7@cea.fr> <1229094404.3360.35.camel@supelec>
> > I get warnings such as...
> I attached socket.h and unistd.h from my system.

Still no luck (different error messages coming from
the incompatibility between the remainder of my system
include files and yours). Some suggestions come later
in this message.

> > 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?
> What platform are you on ? So I can test the self-contained analysis
> project before sending it to you.

That's the wrong way to look at it. Further down the road, the person
best able to help you may be someone who uses OpenBSD, 
or someone who is stuck in a conference room listening to boring
talks and with only Windows on his notebook.
But if you really want an answer to your question, please
assume that I have a Windows machine with no development
environment installed except a preprocessor, and that I know how
to use it.

Or rather don't. It would be a waste of your time.
Do one of the following instead: 

1/ Use your preprocessor (that I assume you know how to
use, but just in case, here's an example that works for me):

Manzana:frama-c-Lithium-20081002+beta1 pascal$ gcc -C -E -I . tests/idct/ieee_1180_1990.c > ieee.i
Manzana:frama-c-Lithium-20081002+beta1 pascal$ gcc -C -E -I . tests/idct/idct.c > idct.i

and send me the equivalent for your project of
the preprocessed files that are here idct.i and ieee.i.

2/ Use the option -print of Frama-C

Manzana:frama-c-Lithium-20081002+beta1 pascal$ bin/toplevel.opt -print tests/idct/*.c -ocode t.c

If the analysis works for you to the point of being able to show you
code wrongly detected as dead, this command should produce
a single compilable, executable C file t.c that is equivalent to your
whole application.

Pascal

PS: Note that Frama-C is intended to be a portable platform.
The target platform for the analysis can be chosen independently from
where you are running the analyzer. You can analyze 64-bit programs
on a 32-bit machine and embedded code intended for an ARM
environment on Windows.