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] Frama-c fails to open a C file

  • Subject: [Frama-c-discuss] Frama-c fails to open a C file
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Mon, 16 Mar 2009 12:36:45 +0100
  • In-reply-to: <1237202864.3508.60.camel@supelec>
  • References: <1237202864.3508.60.camel@supelec>
On Mar 16, 2009, at 12:27 PM, Jonathan-Christofer Demay wrote:

> However, with 'frama-c-gui bsd-base64.c', I got some errors:
>> Parsing
>> [preprocessing] running gcc -C -E -I.   bsd-base64.c
>> /usr/include/ctype.h:48: Error: Constant expression tmp has effects
>> /usr/include/ctype.h:48: Fatal error: Constant initializer tmp not an
>> integer
>> Skipping file "bsd-base64.c" that has errors.

This error is caused by the normalization attempted by
Frama-C. During the normalization, temporary variables
(which can be named "tmp") may be introduced, which
explains the strange error message that you are obtaining.

While we investigate the problem, workarounds are :

1/ to analyze your project as if it was
intended to run on a big-endian configuration, because
this part of the header ctype.h does not cause the same problem.
Use frama-c -machdep ppc_32 and be consistent with that choice
in the headers (and defined macros such as __BIG_ENDIAN,
_LITTLE_ENDIAN...) that are part of your analysis project.

2/ replace the values _ISbit(...) by their value, which is a constant
without effects despite what Frama-C is telling you.

Pascal