#frama-c
Вопрос:
Я хотел бы реализовать простой абстрактный домен, используя функторы, предоставляемые модулем Domain_builder (задокументировано в разделе EVA->Домены), но я не могу открыть модуль. Простой файл ocaml x.ml:
open Domain_builder
и команда frama-c -load-script x.ml выдает ошибку несвязанного модуля Domain_builder. Однако я могу импортировать другие модули, описанные в этом разделе (например, Cvalue).
Похоже, что модуль Domain_builder не экспортируется файлом EVA .mli (https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/value/Eva.mli), но и не является модулем Cvalue.
Я делаю что-то не так, или модуль Domain_builder действительно отсутствует в подписи EVA?
Ответ №1:
К сожалению, вы правы, Domain_builder на данный момент его нельзя использовать за пределами Eva (ПРИМЕЧАНИЕ: если бы он был экспортирован, вам open Eva.Domain_builder в любом случае пришлось бы это сделать).
Что касается того, почему Cvalue доступно: по историческим причинам этот модуль вместе со всеми файлами внутри src/plugins/value_types фактически рассматривается как модули ядра.