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] Support for RISCV
- Subject: [Frama-c-discuss] Support for RISCV
- From: gergo.barany at cea.fr (Gergö Barany)
- Date: Mon, 23 Jan 2017 11:08:09 +0100
- In-reply-to: <9732e061-bac9-7205-b3da-9682f67abe87@linki.tools>
- References: <9732e061-bac9-7205-b3da-9682f67abe87@linki.tools>
On 20/01/17 12:33, Paulo Matos wrote: > What's the best place to start if I want to add support for RISCV? > > Is there any documentation on adding a new backend to Frama-C? Here is a relevant Stack Overflow answer: http://stackoverflow.com/questions/20083994/how-to-control-size-of-basic-arithmetic-types-in-frama-c However, that code is not directly usable because the API has been changed (simplified!). I attached an example machdep (which is just renamed x86_64) in my_machdep.ml. You can rename and adapt this to your preferred RISC-V variant(s). To make Frama-C use this machdep, run it like this: frama-c -load-script my_machdep.ml -machdep some_64_bit_machine <input files and other flags> The -load-script flag loads your machdep definition, the -machdep flag actually selects this particular machdep. You will also get a message like this: [kernel] warning: machdep some_64_bit_machine has no registered macro. Using __FC_MACHDEP_SOME_64_BIT_MACHINE for pre-processing This means that you can use #ifdef __FC_MACHDEP_SOME_64_BIT_MACHINE to guard code specific to this machine. This probably should not be a warning. I'll try to add a short description of this process to the Frama-C plugin development guide. Let us know if this works for you! Gergö -------------- next part -------------- open Cil_types (* Adapted from x86_64 machdep in src/kernel_internals/runtime/machdeps.ml *) let some_64_bit_machine = { version = "compatible with gcc 4.0.3 (maybe)"; compiler = "generic"; (* use "gcc" to allow some GCC extensions *) cpp_arch_flags = ["-m64"]; sizeof_short = 2; sizeof_int = 4; sizeof_long = 8; sizeof_longlong = 8; sizeof_ptr = 8; sizeof_float = 4; sizeof_double = 8; sizeof_longdouble = 16; sizeof_void = 1; sizeof_fun = 1; size_t = "unsigned long"; wchar_t = "int"; ptrdiff_t = "long"; alignof_short = 2; alignof_int = 4; alignof_long = 8; alignof_longlong = 8; alignof_ptr = 8; alignof_float = 4; alignof_double = 8; alignof_longdouble = 16; alignof_str = 1; alignof_fun = 1; alignof_aligned= 16; char_is_unsigned = false; const_string_literals = true; little_endian = true; underscore_name = false ; has__builtin_va_list = true; __thread_is_keyword = true; } let () = File.new_machdep "some_64_bit_machine" some_64_bit_machine
- References:
- [Frama-c-discuss] Support for RISCV
- From: pmatos at linki.tools (Paulo Matos)
- [Frama-c-discuss] Support for RISCV
- Prev by Date: [Frama-c-discuss] Support for RISCV
- Next by Date: [Frama-c-discuss] Support for RISCV
- Previous by thread: [Frama-c-discuss] Support for RISCV
- Next by thread: [Frama-c-discuss] Support for RISCV
- Index(es):