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

Hello, Sylvain.

On Fri, Feb 3, 2012 at 3:07 PM, sylvain nahas
<sylvain.nahas at>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

> 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,

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>