Как настроить зависимость от машины в Frama-C?

Question

У меня есть 16-разрядный MPU, который отличается от x86_16 размером size_t, ptrdiff_t и т. Д. Может ли кто-нибудь дать мне подробные и четкие инструкции о настройке машинной зависимости в Frama-C для моего MPU?

Answer 1

В настоящее время нет способа сделать это непосредственно из командной строки: вам нужно написать небольшой сценарий OCaml, который по существу определит новый Cil_types.mach (запись, содержащую необходимую информацию о вашей архитектуре) и зарегистрируйте ее через File.new_machdep. Если у вас есть файл my_machdep.ml смотря как то:

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: = $ (скорлупа Frama-с -print-шер-путь)

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 среди списка известных машиппов.

UPDATE Если вы используете несколько заголовков из стандартной библиотеки FRAMA-C, вы также должны обновить $(frama-c -print-share-path)/libc/__fc_machdep.h для того, чтобы определить соответствующие макросы (связанные с limits.h и stdint.h в основном).