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