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

Я пытаюсь создать плагин frama-c. Этот плагин зависит от плагина Frama-c Value. Я хочу получить и распечатать набор значений всех 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 из другого плагина?

1 ответ

Решение

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

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

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

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

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

Другие вопросы по тегам