--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on January 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Support for RISCV



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