Как использовать функции в Value.Eval_expr, Value.Eval_op и т. Д. Модули плагина Value Frama-c

Question

Я пытаюсь создать плагин frama-c. Этот плагин зависит от плагина Value Frama-c. Я хочу получить и распечатать набор значений всех lvalue (s) в исходном коде C. Для этого я хочу использовать функции, доступные в Value.Eval_exprs, Value.Eval_op и т. Д., Например Eval_exprs.lval_to_precise_loc.

К сожалению, я не могу найти способ использовать эти функции в своем плагине. Я попытался выполнить шаги, упомянутые в разделе 4.10.1 (Регистрация через файл .mli) руководства по разработке плагинов Frama-c, и добавил PLUGIN_DEPENDENCIES:=Value в мой файл Makefile, но я заметил, что файл Value.mli пуст, и никакая функция не открывается через этот файл. После этого я смотрел на db.ml файл в каталоге kernel и не смогли найти какой-либо модуль, который может использоваться для доступа ко всем функциям, доступным в Eval_exprs, Eval_op и т.д.

Есть ли способ получить доступ к этим функции Value плагина от других плагин?

Answer 1

Множественные механизмы доступны для использования результатов плагин Frama-C Programatically:

1. через модуль Db, который содержит функции для доступа к результатам многих «основных» плагинов
2. через вызовы «динамический» API (модуль Dynamic)
3. через интерфейс плагина (например, Value.mli в вашем случае)

Первые два подхода устарели и в конечном итоге исчезнут. Кроме того, подход 1. недоступен для пользовательских плагинов. Вот почему руководство разработчика подчеркивает подход 3.

В настоящее время результаты Value доступны с использованием подхода 1 (только). Внутри вашего плагина вы можете просто написать !Db.Value.eval_expr или !Db.Value.eval_lval, чтобы оценить выражение и левое значение соответственно. Это будет работать автоматически. Вы должны объявить значение как зависимость вашего плагина (PLUGIN_DEPENDENCIES:=Value, как вы узнали), поскольку это потребуется в следующей версии Frama-C. Все внутренние модулей, таких как Eval_exprs, являются не экспортировано, намеренно. Большинство применений результатов Value могут быть записаны с использованием функций, доступных в Db.Value.

И, наконец, lval_to_precise_loc - довольно продвинутая функция, так как возвращаемые местоположения имеют тип, который трудно использовать. Db.Value.lval_to_loc - почти всегда лучший выбор.