How customize machine dependency in Frama-C?

Question

I have got a 16-bit MPU wich is different from x86_16 in size of size_t, ptrdiff_t etc. Can anybody give me details and clear instructions about how to customise machine dependency in Frama-C for my MPU?

Answer 1

There is currently no way to do that directly from the command line: you have to write a small OCaml script that will essentially define a new Cil_types.mach (a record containing the necessary information about your architecture) and register it through File.new_machdep. Assuming you have a file my_machdep.ml looking like that:

let my_machdep = {
  Cil_types.sizeof_short = 2;
  sizeof_int = 2;
  sizeof_long = 4;
  (* ... See `cil_types.mli` for the complete list of fields to define *)
}

let () = File.new_machdep "my_machdep" my_machdep

You will then be able to launch Frama-C that way to use the new machdep:

frama-c -load-script my_machdep.ml -machdep my_machdep [normal options]

If you want to have the new machdep permanently available, you can make it a Frama-C plugin. For that, you need a Makefile of the following form:

FRAMAC_SHARE:=$(shell frama-c -print-share-path)

PLUGIN_NAME=Custom_machdep
PLUGIN_CMO=my_machdep

include $(FRAMAC_SHARE)/Makefile.dynamic

my_machdep must be the name of your .ml file. Be sure to choose a different name for PLUGIN_NAME. Then, create an empty Custom_machdep.mli file (touch Custom_machdep.mli should do the trick). Afterwards, make && make install should compile and install the plug-in so that it will be automatically loaded by Frama-C. You can verify this by launching frama-c -machdep help that should output my_machdep among the list of known machdeps.

UPDATE If you are using some headers from Frama-C's standard library, you will also have to update $(frama-c -print-share-path)/libc/__fc_machdep.h in order to define appropriate macros (related to limits.h and stdint.h mostly).