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] CHAR_BIT != 8

  • Subject: [Frama-c-discuss] CHAR_BIT != 8
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 6 Feb 2012 17:36:24 +0100
  • In-reply-to: <CAO5eZdE_hY21TLURgUuQKR=gcwbMigR+wX1iVBQHpGx=44RJoQ@mail.gmail.com>
  • References: <CAO5eZdE_hY21TLURgUuQKR=gcwbMigR+wX1iVBQHpGx=44RJoQ@mail.gmail.com>
Hello,

On Mon, Feb 6, 2012 at 2:59 PM, Ned <ned at tropic.org.uk> wrote:

> I'm interested in using frama-c with a couple of architectures with
> CHAR_BIT being some value other than 8 (16 in one case, 24 in another).  I
> can see that the first problem will be CIL; there's no mention of CHAR_BIT
> in machdep_*.ml, and there are a lot of suspicious multiplications by 8 in
> the code.  Presuming I am able to fix CIL (in fact I have a likely looking
> patch developed by a former colleague, although I don't know whether it's
> complete), does anyone know what will break next?


Yes, the first and foremost issue is that of all the suspicious eights in
the front-end.

There are more of these eights in the plug-ins themselves, and I cannot
guarantee that you won't find suspicious shifts by 3. Just replace those by
shifts by log2(24) when you encounter them :)

And then, there are subtle bugs in the implementation of typing rules. As
an example, we have already fixed bugs that only occurred for architectures
where sizeof(long)==sizeof(long long), but that were invisible otherwise.
Who knows what will come up for architectures where
sizeof(char)==sizeof(short)==sizeof(int)?
Similarly, I think we have only ever tested architectures where chars are
signed by default.

Since your interest in unusual CHAR_BITs presumably stems from your having
at hand processors with these characteristics, and C compilers for these
processors, you may be able to discover bugs following the recipes
described in http://blog.frama-c.com/public/csmith.pdf (the scripts are
available from the annex at
http://blog.frama-c.com/index.php?pages/Csmith-testing ). However, if the C
compilers have not previously been tested with Csmith, you can expect most
of the differences between them and Frama-C that will initially come up to
be attributable to bugs in the compilers. As the annex to the article says,
you should reduce the problematic random programs yourself, and then you
will see whether it's the compiler or Frama-C that gets it wrong.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120206/cd88242c/attachment.htm>