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] Defining a new architecture
- Subject: [Frama-c-discuss] Defining a new architecture
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Fri, 3 Feb 2012 23:02:02 +0100
- In-reply-to: <CAFaEDLCyP8fTHPpWnvpZzCoo9hNEQsTHDWpUsyJ9H4mGjfVMGg@mail.gmail.com>
- References: <CAFaEDLCyP8fTHPpWnvpZzCoo9hNEQsTHDWpUsyJ9H4mGjfVMGg@mail.gmail.com>
Hello, Sylvain. On Fri, Feb 3, 2012 at 3:07 PM, sylvain nahas <sylvain.nahas at googlemail.com>wrote: > 1. Has somebody already used Frama-C on 8 bits processor architectures? > Is it expected to work? > It is not expected to work until it has been tested. For all we know, it could fail for all programs, or silently mess up one target program in ten. > 2. How is it currently possible to add a new architecture as a > parameter to -machdep - alternatively, is there a way to achieve the > same level of parametrization without creating a machdep-*.ml file > (maybe with command line switches)? > > I have had a look at the machdep-*.ml files. The content is clear > enough but I am wondering how a user is supposed to add a definition. > By modifying the source code? Is it then enough to add a new file and > tweak a Makefile or is there more wizardry involved? > You need to test it and debug the front-end bugs that only occur with the new architecture and have never been revealed before. This part of Frama-C is not considered user-serviceable. We won't explain how to change it with the current system, that is not intended to be convenient (free hint). Having us develop a new target architecture is an excellent excuse for a "support and minor evolutions" contract with us. In fact, this kind of adaptation fits right into the standard one that several partners have already adopted. Still, Frama-C is open-source and it is your privilege to mess with it on your own. Best regards, Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120203/61bc4132/attachment.htm>
- References:
- [Frama-c-discuss] Defining a new architecture
- From: sylvain.nahas at googlemail.com (sylvain nahas)
- [Frama-c-discuss] Defining a new architecture
- Prev by Date: [Frama-c-discuss] Can the tools be used with intrinsic in customer simulators
- Next by Date: [Frama-c-discuss] CHAR_BIT != 8
- Previous by thread: [Frama-c-discuss] Defining a new architecture
- Next by thread: [Frama-c-discuss] CHAR_BIT != 8
- Index(es):