How to configure machine dependency in Frama-C?

Question

I have a 16-bit MPU that is different from x86_16 in size size_t, ptrdiff_tetc. Can someone give me detailed and clear instructions on how to configure machine dependency in Frama-C for my MPU?

Answer 1

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

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

Frama-C , machdep:

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

, machdep , Frama-C. Makefile :

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

PLUGIN_NAME=Custom_machdep
PLUGIN_CMO=my_machdep

include $(FRAMAC_SHARE)/Makefile.dynamic

my_machdep .ml. PLUGIN_NAME. Custom_machdep.mli (touch Custom_machdep.mli ). make && make install , Frama-C. , frama-c -machdep help, my_machdep machdeps.

UPDATE Frama-C, $(frama-c -print-share-path)/libc/__fc_machdep.h, ( limits.h stdint.h).